<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>Poly: Polymorphism and Higher-Order Functions</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>
</head>

<body>

<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 1: Logical Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>

<div id="main">

<h1 class="libtitle">Poly<span class="subtitle">Polymorphism and Higher-Order Functions</span></h1>


<div class="code">

<span class="id" title="keyword">From</span> <span class="id" title="var">LF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Lists.html#"><span class="id" title="library">Lists</span></a>.<br/>
</div>

<div class="doc">
<a id="lab102"></a><h1 class="section">Polymorphism</h1>

<div class="paragraph"> </div>

 In this chapter we continue our development of basic
    concepts of functional programming.  The critical new ideas are
    <i>polymorphism</i> (abstracting functions over the types of the data
    they manipulate) and <i>higher-order functions</i> (treating functions
    as data).  We begin with polymorphism. 
</div>

<div class="doc">
<a id="lab103"></a><h2 class="section">Polymorphic Lists</h2>

<div class="paragraph"> </div>

 For the last chapter, we've been working with lists
    containing just numbers.  Obviously, interesting programs also
    need to be able to manipulate lists with elements from other
    types -- lists of booleans, lists of lists, etc.  We <i>could</i> just
    define a new inductive datatype for each of these, for
    example... 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="boollist" class="idref" href="#boollist"><span class="id" title="inductive">boollist</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="bool_nil" class="idref" href="#bool_nil"><span class="id" title="constructor">bool_nil</span></a><br/>
&nbsp;&nbsp;| <a id="bool_cons" class="idref" href="#bool_cons"><span class="id" title="constructor">bool_cons</span></a> (<a id="b:3" class="idref" href="#b:3"><span class="id" title="binder">b</span></a> : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>) (<a id="l:4" class="idref" href="#l:4"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#boollist:1"><span class="id" title="inductive">boollist</span></a>).<br/>
</div>

<div class="doc">
... but this would quickly become tedious, partly because we
    have to make up different constructor names for each datatype, but
    mostly because we would also need to define new versions of all
    our list manipulating functions (<span class="inlinecode"><span class="id" title="var">length</span></span>, <span class="inlinecode"><span class="id" title="var">rev</span></span>, etc.) and all
    their properties (<span class="inlinecode"><span class="id" title="var">rev_length</span></span>, <span class="inlinecode"><span class="id" title="var">app_assoc</span></span>, etc.) for each
    new datatype definition. 
<div class="paragraph"> </div>

 To avoid all this repetition, Coq supports <i>polymorphic</i>
    inductive type definitions.  For example, here is a <i>polymorphic
    list</i> datatype. 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="list" class="idref" href="#list"><span class="id" title="inductive">list</span></a> (<a id="X:5" class="idref" href="#X:5"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="nil" class="idref" href="#nil"><span class="id" title="constructor">nil</span></a><br/>
&nbsp;&nbsp;| <a id="cons" class="idref" href="#cons"><span class="id" title="constructor">cons</span></a> (<a id="x:8" class="idref" href="#x:8"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#X:5"><span class="id" title="variable">X</span></a>) (<a id="l:9" class="idref" href="#l:9"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list:6"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:5"><span class="id" title="variable">X</span></a>).<br/>
</div>

<div class="doc">
This is exactly like the definition of <span class="inlinecode"><span class="id" title="var">natlist</span></span> from the
    previous chapter, except that the <span class="inlinecode"><span class="id" title="var">nat</span></span> argument to the <span class="inlinecode"><span class="id" title="var">cons</span></span>
    constructor has been replaced by an arbitrary type <span class="inlinecode"><span class="id" title="var">X</span></span>, a binding
    for <span class="inlinecode"><span class="id" title="var">X</span></span> has been added to the function header on the first line,
    and the occurrences of <span class="inlinecode"><span class="id" title="var">natlist</span></span> in the types of the constructors
    have been replaced by <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span>.

<div class="paragraph"> </div>

    What sort of thing is <span class="inlinecode"><span class="id" title="var">list</span></span> itself?  A good way to think about it
    is that the definition of <span class="inlinecode"><span class="id" title="var">list</span></span> is a <i>function</i> from <span class="inlinecode"><span class="id" title="keyword">Type</span></span>s to
    <span class="inlinecode"><span class="id" title="keyword">Inductive</span></span> definitions; or, to put it more concisely, <span class="inlinecode"><span class="id" title="var">list</span></span> is a
    function from <span class="inlinecode"><span class="id" title="keyword">Type</span></span>s to <span class="inlinecode"><span class="id" title="keyword">Type</span></span>s.  For any particular type <span class="inlinecode"><span class="id" title="var">X</span></span>,
    the type <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> is the <span class="inlinecode"><span class="id" title="keyword">Inductive</span></span>ly defined set of lists whose
    elements are of type <span class="inlinecode"><span class="id" title="var">X</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> : <span class="id" title="keyword">Type</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span>.<br/>
</div>

<div class="doc">
The <span class="inlinecode"><span class="id" title="var">X</span></span> in the definition of <span class="inlinecode"><span class="id" title="var">list</span></span> automatically becomes a
    parameter to the constructors <span class="inlinecode"><span class="id" title="var">nil</span></span> and <span class="inlinecode"><span class="id" title="var">cons</span></span> -- that is, <span class="inlinecode"><span class="id" title="var">nil</span></span>
    and <span class="inlinecode"><span class="id" title="var">cons</span></span> are now polymorphic constructors; when we use them, we
    must now provide a first argument that is the type of the list
    they are building. For example, <span class="inlinecode"><span class="id" title="var">nil</span></span> <span class="inlinecode"><span class="id" title="var">nat</span></span> constructs the empty
    list of type <span class="inlinecode"><span class="id" title="var">nat</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> (<a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
</div>

<div class="doc">
Similarly, <span class="inlinecode"><span class="id" title="var">cons</span></span> <span class="inlinecode"><span class="id" title="var">nat</span></span> adds an element of type <span class="inlinecode"><span class="id" title="var">nat</span></span> to a list of
    type <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">nat</span></span>. Here is an example of forming a list containing
    just the natural number 3. 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> 3 (<a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)) : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
</div>

<div class="doc">
What might the type of <span class="inlinecode"><span class="id" title="var">nil</span></span> be? We can read off the type
    <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> from the definition, but this omits the binding for <span class="inlinecode"><span class="id" title="var">X</span></span>
    which is the parameter to <span class="inlinecode"><span class="id" title="var">list</span></span>. <span class="inlinecode"><span class="id" title="keyword">Type</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> does not
    explain the meaning of <span class="inlinecode"><span class="id" title="var">X</span></span>. <span class="inlinecode">(<span class="id" title="var">X</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="keyword">Type</span>)</span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> comes
    closer. Coq's notation for this situation is <span class="inlinecode"><span class="id" title="keyword">∀</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="keyword">Type</span>,</span>
    <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> : <span class="id" title="keyword">∀</span> <a id="X:10" class="idref" href="#X:10"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>, <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:10"><span class="id" title="variable">X</span></a>.<br/>
</div>

<div class="doc">
Similarly, the type of <span class="inlinecode"><span class="id" title="var">cons</span></span> from the definition looks like
    <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span>, but using this convention to explain the
    meaning of <span class="inlinecode"><span class="id" title="var">X</span></span> results in the type <span class="inlinecode"><span class="id" title="keyword">∀</span></span> <span class="inlinecode"><span class="id" title="var">X</span>,</span> <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">list</span></span>
    <span class="inlinecode"><span class="id" title="var">X</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> : <span class="id" title="keyword">∀</span> <a id="X:11" class="idref" href="#X:11"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>, <a class="idref" href="Poly.html#X:11"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:11"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:11"><span class="id" title="variable">X</span></a>.<br/>
</div>

<div class="doc">
(A side note on notations: In .v files, the "forall"
    quantifier is spelled out in letters.  In the corresponding HTML
    files (and in the way some IDEs show .v files, depending on the
    settings of their display controls), <span class="inlinecode"><span class="id" title="keyword">∀</span></span> is usually typeset
    as the standard mathematical "upside down A," though you'll still
    see the spelled-out "forall" in a few places.  This is just a
    quirk of typesetting -- there is no difference in meaning.) 
<div class="paragraph"> </div>

 Having to supply a type argument for every single use of a
    list constructor would be rather burdensome; we will soon see ways
    of reducing this annotation burden. 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> 2 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> 1 (<a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
</div>

<div class="doc">
We can now go back and make polymorphic versions of all the
    list-processing functions that we wrote before.  Here is <span class="inlinecode"><span class="id" title="tactic">repeat</span></span>,
    for example: 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="repeat" class="idref" href="#repeat"><span class="id" title="definition">repeat</span></a> (<a id="X:12" class="idref" href="#X:12"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>) (<a id="x:13" class="idref" href="#x:13"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#X:12"><span class="id" title="variable">X</span></a>) (<a id="count:14" class="idref" href="#count:14"><span class="id" title="binder">count</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:12"><span class="id" title="variable">X</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#count:14"><span class="id" title="variable">count</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0 ⇒ <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="Poly.html#X:12"><span class="id" title="variable">X</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">count'</span> ⇒ <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="Poly.html#X:12"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#x:13"><span class="id" title="variable">x</span></a> (<a class="idref" href="Poly.html#repeat:15"><span class="id" title="definition">repeat</span></a> <a class="idref" href="Poly.html#X:12"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#x:13"><span class="id" title="variable">x</span></a> <span class="id" title="var">count'</span>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
As with <span class="inlinecode"><span class="id" title="var">nil</span></span> and <span class="inlinecode"><span class="id" title="var">cons</span></span>, we can use <span class="inlinecode"><span class="id" title="tactic">repeat</span></span> by applying it
    first to a type and then to an element of this type (and a number): 
</div>
<div class="code">

<span class="id" title="keyword">Example</span> <a id="test_repeat1" class="idref" href="#test_repeat1"><span class="id" title="definition">test_repeat1</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#repeat"><span class="id" title="definition">repeat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> 4 2 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> 4 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> 4 (<a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)).<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
To use <span class="inlinecode"><span class="id" title="tactic">repeat</span></span> to build other kinds of lists, we simply
    instantiate it with an appropriate type parameter: 
</div>
<div class="code">

<span class="id" title="keyword">Example</span> <a id="test_repeat2" class="idref" href="#test_repeat2"><span class="id" title="definition">test_repeat2</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#repeat"><span class="id" title="definition">repeat</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a> 1 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a> (<a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>).<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab104"></a><h4 class="section">Exercise: 2 stars, standard (mumble_grumble)</h4>
 Consider the following two inductively defined types. 
</div>
<div class="code">

<span class="id" title="keyword">Module</span> <a id="MumbleGrumble" class="idref" href="#MumbleGrumble"><span class="id" title="module">MumbleGrumble</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="MumbleGrumble.mumble" class="idref" href="#MumbleGrumble.mumble"><span class="id" title="inductive">mumble</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="MumbleGrumble.a" class="idref" href="#MumbleGrumble.a"><span class="id" title="constructor">a</span></a><br/>
&nbsp;&nbsp;| <a id="MumbleGrumble.b" class="idref" href="#MumbleGrumble.b"><span class="id" title="constructor">b</span></a> (<a id="x:19" class="idref" href="#x:19"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#mumble:17"><span class="id" title="inductive">mumble</span></a>) (<a id="y:20" class="idref" href="#y:20"><span class="id" title="binder">y</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)<br/>
&nbsp;&nbsp;| <a id="MumbleGrumble.c" class="idref" href="#MumbleGrumble.c"><span class="id" title="constructor">c</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="MumbleGrumble.grumble" class="idref" href="#MumbleGrumble.grumble"><span class="id" title="inductive">grumble</span></a> (<a id="X:21" class="idref" href="#X:21"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="MumbleGrumble.d" class="idref" href="#MumbleGrumble.d"><span class="id" title="constructor">d</span></a> (<a id="m:24" class="idref" href="#m:24"><span class="id" title="binder">m</span></a> : <a class="idref" href="Poly.html#MumbleGrumble.mumble"><span class="id" title="inductive">mumble</span></a>)<br/>
&nbsp;&nbsp;| <a id="MumbleGrumble.e" class="idref" href="#MumbleGrumble.e"><span class="id" title="constructor">e</span></a> (<a id="x:25" class="idref" href="#x:25"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#X:21"><span class="id" title="variable">X</span></a>).<br/>
</div>

<div class="doc">
Which of the following are well-typed elements of <span class="inlinecode"><span class="id" title="var">grumble</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> for
    some type <span class="inlinecode"><span class="id" title="var">X</span></span>?  (Add YES or NO to each line.)
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">d</span></span> <span class="inlinecode">(<span class="id" title="var">b</span></span> <span class="inlinecode"><span class="id" title="var">a</span></span> <span class="inlinecode">5)</span>

</li>
<li> <span class="inlinecode"><span class="id" title="var">d</span></span> <span class="inlinecode"><span class="id" title="var">mumble</span></span> <span class="inlinecode">(<span class="id" title="var">b</span></span> <span class="inlinecode"><span class="id" title="var">a</span></span> <span class="inlinecode">5)</span>

</li>
<li> <span class="inlinecode"><span class="id" title="var">d</span></span> <span class="inlinecode"><span class="id" title="var">bool</span></span> <span class="inlinecode">(<span class="id" title="var">b</span></span> <span class="inlinecode"><span class="id" title="var">a</span></span> <span class="inlinecode">5)</span>

</li>
<li> <span class="inlinecode"><span class="id" title="var">e</span></span> <span class="inlinecode"><span class="id" title="var">bool</span></span> <span class="inlinecode"><span class="id" title="var">true</span></span>

</li>
<li> <span class="inlinecode"><span class="id" title="var">e</span></span> <span class="inlinecode"><span class="id" title="var">mumble</span></span> <span class="inlinecode">(<span class="id" title="var">b</span></span> <span class="inlinecode"><span class="id" title="var">c</span></span> <span class="inlinecode">0)</span>

</li>
<li> <span class="inlinecode"><span class="id" title="var">e</span></span> <span class="inlinecode"><span class="id" title="var">bool</span></span> <span class="inlinecode">(<span class="id" title="var">b</span></span> <span class="inlinecode"><span class="id" title="var">c</span></span> <span class="inlinecode">0)</span>

</li>
<li> <span class="inlinecode"><span class="id" title="var">c</span></span>  

</li>
</ul>
</div>
<div class="code">
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Poly.html#MumbleGrumble"><span class="id" title="module">MumbleGrumble</span></a>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_mumble_grumble" class="idref" href="#manual_grade_for_mumble_grumble"><span class="id" title="definition">manual_grade_for_mumble_grumble</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab105"></a><h3 class="section">Type Annotation Inference</h3>

<div class="paragraph"> </div>

 Let's write the definition of <span class="inlinecode"><span class="id" title="tactic">repeat</span></span> again, but this time we
    won't specify the types of any of the arguments.  Will Coq still
    accept it? 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="repeat'" class="idref" href="#repeat'"><span class="id" title="definition">repeat'</span></a> <a id="X:26" class="idref" href="#X:26"><span class="id" title="binder">X</span></a> <a id="x:27" class="idref" href="#x:27"><span class="id" title="binder">x</span></a> <a id="count:28" class="idref" href="#count:28"><span class="id" title="binder">count</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:26"><span class="id" title="variable">X</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#count:28"><span class="id" title="variable">count</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0        ⇒ <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="Poly.html#X:26"><span class="id" title="variable">X</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">count'</span> ⇒ <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="Poly.html#X:26"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#x:27"><span class="id" title="variable">x</span></a> (<a class="idref" href="Poly.html#repeat':29"><span class="id" title="definition">repeat'</span></a> <a class="idref" href="Poly.html#X:26"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#x:27"><span class="id" title="variable">x</span></a> <span class="id" title="var">count'</span>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
Indeed it will.  Let's see what type Coq has assigned to <span class="inlinecode"><span class="id" title="var">repeat'</span></span>: 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> <a class="idref" href="Poly.html#repeat'"><span class="id" title="definition">repeat'</span></a><br/>
&nbsp;&nbsp;: <span class="id" title="keyword">∀</span> <a id="X:31" class="idref" href="#X:31"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>, <a class="idref" href="Poly.html#X:31"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:31"><span class="id" title="variable">X</span></a>.<br/>
<span class="id" title="keyword">Check</span> <a class="idref" href="Poly.html#repeat"><span class="id" title="definition">repeat</span></a><br/>
&nbsp;&nbsp;: <span class="id" title="keyword">∀</span> <a id="X:32" class="idref" href="#X:32"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>, <a class="idref" href="Poly.html#X:32"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:32"><span class="id" title="variable">X</span></a>.<br/>
</div>

<div class="doc">
It has exactly the same type as <span class="inlinecode"><span class="id" title="tactic">repeat</span></span>.  Coq was able to
    use <i>type inference</i> to deduce what the types of <span class="inlinecode"><span class="id" title="var">X</span></span>, <span class="inlinecode"><span class="id" title="var">x</span></span>, and
    <span class="inlinecode"><span class="id" title="var">count</span></span> must be, based on how they are used.  For example, since
    <span class="inlinecode"><span class="id" title="var">X</span></span> is used as an argument to <span class="inlinecode"><span class="id" title="var">cons</span></span>, it must be a <span class="inlinecode"><span class="id" title="keyword">Type</span></span>, since
    <span class="inlinecode"><span class="id" title="var">cons</span></span> expects a <span class="inlinecode"><span class="id" title="keyword">Type</span></span> as its first argument; matching <span class="inlinecode"><span class="id" title="var">count</span></span>
    with <span class="inlinecode">0</span> and <span class="inlinecode"><span class="id" title="var">S</span></span> means it must be a <span class="inlinecode"><span class="id" title="var">nat</span></span>; and so on.

<div class="paragraph"> </div>

    This powerful facility means we don't always have to write
    explicit type annotations everywhere, although explicit type
    annotations can still be quite useful as documentation and sanity
    checks, so we will continue to use them much of the time. 
</div>

<div class="doc">
<a id="lab106"></a><h3 class="section">Type Argument Synthesis</h3>

<div class="paragraph"> </div>

 To use a polymorphic function, we need to pass it one or
    more types in addition to its other arguments.  For example, the
    recursive call in the body of the <span class="inlinecode"><span class="id" title="tactic">repeat</span></span> function above must
    pass along the type <span class="inlinecode"><span class="id" title="var">X</span></span>.  But since the second argument to
    <span class="inlinecode"><span class="id" title="tactic">repeat</span></span> is an element of <span class="inlinecode"><span class="id" title="var">X</span></span>, it seems entirely obvious that the
    first argument can only be <span class="inlinecode"><span class="id" title="var">X</span></span> -- why should we have to write it
    explicitly?

<div class="paragraph"> </div>

    Fortunately, Coq permits us to avoid this kind of redundancy.  In
    place of any type argument we can write a "hole" <span class="inlinecode"><span class="id" title="var">_</span></span>, which can be
    read as "Please try to figure out for yourself what belongs here."
    More precisely, when Coq encounters a <span class="inlinecode"><span class="id" title="var">_</span></span>, it will attempt to
    <i>unify</i> all locally available information -- the type of the
    function being applied, the types of the other arguments, and the
    type expected by the context in which the application appears --
    to determine what concrete type should replace the <span class="inlinecode"><span class="id" title="var">_</span></span>.

<div class="paragraph"> </div>

    This may sound similar to type annotation inference -- and, indeed,
    the two procedures rely on the same underlying mechanisms.  Instead
    of simply omitting the types of some arguments to a function, like
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">repeat'</span> <span class="id" title="var">X</span> <span class="id" title="var">x</span> <span class="id" title="var">count</span> : <span class="id" title="var">list</span> <span class="id" title="var">X</span> :=
</span>    we can also replace the types with holes
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">repeat'</span> (<span class="id" title="var">X</span> : <span class="id" title="var">_</span>) (<span class="id" title="var">x</span> : <span class="id" title="var">_</span>) (<span class="id" title="var">count</span> : <span class="id" title="var">_</span>) : <span class="id" title="var">list</span> <span class="id" title="var">X</span> :=
</span>    to tell Coq to attempt to infer the missing information.

<div class="paragraph"> </div>

    Using holes, the <span class="inlinecode"><span class="id" title="tactic">repeat</span></span> function can be written like this: 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="repeat''" class="idref" href="#repeat''"><span class="id" title="definition">repeat''</span></a> <a id="X:33" class="idref" href="#X:33"><span class="id" title="binder">X</span></a> <a id="x:34" class="idref" href="#x:34"><span class="id" title="binder">x</span></a> <a id="count:35" class="idref" href="#count:35"><span class="id" title="binder">count</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:33"><span class="id" title="variable">X</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#count:35"><span class="id" title="variable">count</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0        ⇒ <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <span class="id" title="var">_</span><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">count'</span> ⇒ <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">_</span> <a class="idref" href="Poly.html#x:34"><span class="id" title="variable">x</span></a> (<a class="idref" href="Poly.html#repeat'':36"><span class="id" title="definition">repeat''</span></a> <span class="id" title="var">_</span> <a class="idref" href="Poly.html#x:34"><span class="id" title="variable">x</span></a> <span class="id" title="var">count'</span>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
In this instance, we don't save much by writing <span class="inlinecode"><span class="id" title="var">_</span></span> instead of
    <span class="inlinecode"><span class="id" title="var">X</span></span>.  But in many cases the difference in both keystrokes and
    readability is nontrivial.  For example, suppose we want to write
    down a list containing the numbers <span class="inlinecode">1</span>, <span class="inlinecode">2</span>, and <span class="inlinecode">3</span>.  Instead of
    this... 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="list123" class="idref" href="#list123"><span class="id" title="definition">list123</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> 1 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> 2 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> 3 (<a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>))).<br/>
</div>

<div class="doc">
...we can use holes to write this: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="list123'" class="idref" href="#list123'"><span class="id" title="definition">list123'</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">_</span> 1 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">_</span> 2 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">_</span> 3 (<a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <span class="id" title="var">_</span>))).<br/>
</div>

<div class="doc">
<a id="lab107"></a><h3 class="section">Implicit Arguments</h3>

<div class="paragraph"> </div>

 In fact, we can go further and even avoid writing <span class="inlinecode"><span class="id" title="var">_</span></span>'s in most
    cases by telling Coq <i>always</i> to infer the type argument(s) of a
    given function.

<div class="paragraph"> </div>

    The <span class="inlinecode"><span class="id" title="var">Arguments</span></span> directive specifies the name of the function (or
    constructor) and then lists the (leading) argument names to be
    treated as implicit, each surrounded by curly braces. 
</div>
<div class="code">

<span class="id" title="var">Arguments</span> <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> {<span class="id" title="var">X</span>}.<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> {<span class="id" title="var">X</span>}.<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Poly.html#repeat"><span class="id" title="definition">repeat</span></a> {<span class="id" title="var">X</span>}.<br/>
</div>

<div class="doc">
Now we don't have to supply type arguments at all: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="list123''" class="idref" href="#list123''"><span class="id" title="definition">list123''</span></a> := <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> 1 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> 2 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> 3 <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>)).<br/>
</div>

<div class="doc">
Alternatively, we can declare an argument to be implicit
    when defining the function itself, by surrounding it in curly
    braces instead of parens.  For example: 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="repeat'''" class="idref" href="#repeat'''"><span class="id" title="definition">repeat'''</span></a> {<a id="X:38" class="idref" href="#X:38"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>} (<a id="x:39" class="idref" href="#x:39"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#X:38"><span class="id" title="variable">X</span></a>) (<a id="count:40" class="idref" href="#count:40"><span class="id" title="binder">count</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:38"><span class="id" title="variable">X</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#count:40"><span class="id" title="variable">count</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0        ⇒ <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">count'</span> ⇒ <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="Poly.html#x:39"><span class="id" title="variable">x</span></a> (<a class="idref" href="Poly.html#repeat''':41"><span class="id" title="definition">repeat'''</span></a> <a class="idref" href="Poly.html#x:39"><span class="id" title="variable">x</span></a> <span class="id" title="var">count'</span>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
(Note that we didn't even have to provide a type argument to the
    recursive call to <span class="inlinecode"><span class="id" title="var">repeat'''</span></span>.  Indeed, it would be invalid to
    provide one, because Coq is not expecting it.)

<div class="paragraph"> </div>

    We will use the latter style whenever possible, but we will
    continue to use explicit <span class="inlinecode"><span class="id" title="var">Argument</span></span> declarations for <span class="inlinecode"><span class="id" title="keyword">Inductive</span></span>
    constructors.  The reason for this is that marking the parameter
    of an inductive type as implicit causes it to become implicit for
    the type itself, not just for its constructors.  For instance,
    consider the following alternative definition of the <span class="inlinecode"><span class="id" title="var">list</span></span>
    type: 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="list'" class="idref" href="#list'"><span class="id" title="inductive">list'</span></a> {<a id="X:43" class="idref" href="#X:43"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>} : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="nil'" class="idref" href="#nil'"><span class="id" title="constructor">nil'</span></a><br/>
&nbsp;&nbsp;| <a id="cons'" class="idref" href="#cons'"><span class="id" title="constructor">cons'</span></a> (<a id="x:46" class="idref" href="#x:46"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#X:43"><span class="id" title="variable">X</span></a>) (<a id="l:47" class="idref" href="#l:47"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list':44"><span class="id" title="inductive">list'</span></a>).<br/>
</div>

<div class="doc">
Because <span class="inlinecode"><span class="id" title="var">X</span></span> is declared as implicit for the <i>entire</i> inductive
    definition including <span class="inlinecode"><span class="id" title="var">list'</span></span> itself, we now have to write just
    <span class="inlinecode"><span class="id" title="var">list'</span></span> whether we are talking about lists of numbers or booleans
    or anything else, rather than <span class="inlinecode"><span class="id" title="var">list'</span></span> <span class="inlinecode"><span class="id" title="var">nat</span></span> or <span class="inlinecode"><span class="id" title="var">list'</span></span> <span class="inlinecode"><span class="id" title="var">bool</span></span> or
    whatever; this is a step too far. 
<div class="paragraph"> </div>

 Let's finish by re-implementing a few other standard list
    functions on our new polymorphic lists... 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="app" class="idref" href="#app"><span class="id" title="definition">app</span></a> {<a id="X:48" class="idref" href="#X:48"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>} (<a id="l<sub>1</sub>:49" class="idref" href="#l<sub>1</sub>:49"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:50" class="idref" href="#l<sub>2</sub>:50"><span class="id" title="binder">l<sub>2</sub></span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:48"><span class="id" title="variable">X</span></a>) : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:48"><span class="id" title="variable">X</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#l<sub>1</sub>:49"><span class="id" title="variable">l<sub>1</sub></span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>      ⇒ <a class="idref" href="Poly.html#l<sub>2</sub>:50"><span class="id" title="variable">l<sub>2</sub></span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">h</span> <span class="id" title="var">t</span> ⇒ <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">h</span> (<a class="idref" href="Poly.html#app:51"><span class="id" title="definition">app</span></a> <span class="id" title="var">t</span> <a class="idref" href="Poly.html#l<sub>2</sub>:50"><span class="id" title="variable">l<sub>2</sub></span></a>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="rev" class="idref" href="#rev"><span class="id" title="definition">rev</span></a> {<a id="X:53" class="idref" href="#X:53"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>} (<a id="l:54" class="idref" href="#l:54"><span class="id" title="binder">l</span></a>:<a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:53"><span class="id" title="variable">X</span></a>) : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:53"><span class="id" title="variable">X</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#l:54"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>      ⇒ <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">h</span> <span class="id" title="var">t</span> ⇒ <a class="idref" href="Poly.html#app"><span class="id" title="definition">app</span></a> (<a class="idref" href="Poly.html#rev:55"><span class="id" title="definition">rev</span></a> <span class="id" title="var">t</span>) (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">h</span> <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="length" class="idref" href="#length"><span class="id" title="definition">length</span></a> {<a id="X:57" class="idref" href="#X:57"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>} (<a id="l:58" class="idref" href="#l:58"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:57"><span class="id" title="variable">X</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#l:58"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> ⇒ 0<br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">_</span> <span class="id" title="var">l'</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="Poly.html#length:59"><span class="id" title="definition">length</span></a> <span class="id" title="var">l'</span>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_rev1" class="idref" href="#test_rev1"><span class="id" title="definition">test_rev1</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> 1 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> 2 <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>)) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> 2 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> 1 <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>)<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Example</span> <a id="test_rev2" class="idref" href="#test_rev2"><span class="id" title="definition">test_rev2</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Example</span> <a id="test_length1" class="idref" href="#test_length1"><span class="id" title="definition">test_length1</span></a>: <a class="idref" href="Poly.html#length"><span class="id" title="definition">length</span></a> (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> 1 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> 2 (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> 3 <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>))) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 3.<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab108"></a><h3 class="section">Supplying Type Arguments Explicitly</h3>

<div class="paragraph"> </div>

 One small problem with declaring arguments <span class="inlinecode"><span class="id" title="keyword">Implicit</span></span> is
    that, once in a while, Coq does not have enough local information
    to determine a type argument; in such cases, we need to tell Coq
    that we want to give the argument explicitly just this time.  For
    example, suppose we write this: 
</div>
<div class="code">

<span class="id" title="var">Fail</span> <span class="id" title="keyword">Definition</span> <a id="mynil" class="idref" href="#mynil"><span class="id" title="definition">mynil</span></a> := <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>.<br/>
</div>

<div class="doc">
(The <span class="inlinecode"><span class="id" title="var">Fail</span></span> qualifier that appears before <span class="inlinecode"><span class="id" title="keyword">Definition</span></span> can be
    used with <i>any</i> command, and is used to ensure that that command
    indeed fails when executed. If the command does fail, Coq prints
    the corresponding error message, but continues processing the rest
    of the file.)

<div class="paragraph"> </div>

    Here, Coq gives us an error because it doesn't know what type
    argument to supply to <span class="inlinecode"><span class="id" title="var">nil</span></span>.  We can help it by providing an
    explicit type declaration (so that Coq has more information
    available when it gets to the "application" of <span class="inlinecode"><span class="id" title="var">nil</span></span>): 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="mynil" class="idref" href="#mynil"><span class="id" title="definition">mynil</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> := <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>.<br/>
</div>

<div class="doc">
Alternatively, we can force the implicit arguments to be explicit by
    prefixing the function name with <span class="inlinecode">@</span>. 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> @<a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> : <span class="id" title="keyword">∀</span> <a id="X:61" class="idref" href="#X:61"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>, <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:61"><span class="id" title="variable">X</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="mynil'" class="idref" href="#mynil'"><span class="id" title="definition">mynil'</span></a> := @<a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
</div>

<div class="doc">
Using argument synthesis and implicit arguments, we can
    define convenient notation for lists, as before.  Since we have
    made the constructor type arguments implicit, Coq will know to
    automatically infer these when we use the notations. 
</div>
<div class="code">

<span class="id" title="keyword">Notation</span> <a id=":::x_'::'_x" class="idref" href="#:::x_'::'_x"><span class="id" title="notation">&quot;</span></a>x :: y" := (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="2c60282cbb04e070c60ae01e76f3865a" class="idref" href="#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">&quot;</span></a>[ ]" := <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a>.<br/>
<span class="id" title="keyword">Notation</span> <a id="fa57d319973f6d58544a8887d0d48ea<sub>6</sub>" class="idref" href="#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">&quot;</span></a>[ x ; .. ; y ]" := (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">x</span> .. (<a class="idref" href="Poly.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">y</span> <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a>) ..).<br/>
<span class="id" title="keyword">Notation</span> <a id="f03f7a04ef75ff3ac66ca5c23554e52e" class="idref" href="#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">&quot;</span></a>x ++ y" := (<a class="idref" href="Poly.html#app"><span class="id" title="definition">app</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/>
</div>

<div class="doc">
Now lists can be written just the way we'd hope: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="list123'''" class="idref" href="#list123'''"><span class="id" title="definition">list123'''</span></a> := <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
</div>

<div class="doc">
<a id="lab109"></a><h3 class="section">Exercises</h3>

<div class="paragraph"> </div>

<a id="lab110"></a><h4 class="section">Exercise: 2 stars, standard, optional (poly_exercises)</h4>
 Here are a few simple exercises, just like ones in the <span class="inlinecode"><span class="id" title="var">Lists</span></span>
    chapter, for practice with polymorphism.  Complete the proofs
    below. 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="app_nil_r" class="idref" href="#app_nil_r"><span class="id" title="lemma">app_nil_r</span></a> : <span class="id" title="keyword">∀</span> (<a id="X:62" class="idref" href="#X:62"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>), <span class="id" title="keyword">∀</span> <a id="l:63" class="idref" href="#l:63"><span class="id" title="binder">l</span></a>:<a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:62"><span class="id" title="variable">X</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#l:63"><span class="id" title="variable">l</span></a> <a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#l:63"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="app_assoc" class="idref" href="#app_assoc"><span class="id" title="lemma">app_assoc</span></a> : <span class="id" title="keyword">∀</span> <a id="A:64" class="idref" href="#A:64"><span class="id" title="binder">A</span></a> (<a id="l:65" class="idref" href="#l:65"><span class="id" title="binder">l</span></a> <a id="m:66" class="idref" href="#m:66"><span class="id" title="binder">m</span></a> <a id="n:67" class="idref" href="#n:67"><span class="id" title="binder">n</span></a>:<a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#A:64"><span class="id" title="variable">A</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#l:65"><span class="id" title="variable">l</span></a> <a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Poly.html#m:66"><span class="id" title="variable">m</span></a> <a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Poly.html#n:67"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#l:65"><span class="id" title="variable">l</span></a> <a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Poly.html#m:66"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">)</span></a> <a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Poly.html#n:67"><span class="id" title="variable">n</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Lemma</span> <a id="app_length" class="idref" href="#app_length"><span class="id" title="lemma">app_length</span></a> : <span class="id" title="keyword">∀</span> (<a id="X:68" class="idref" href="#X:68"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>) (<a id="l<sub>1</sub>:69" class="idref" href="#l<sub>1</sub>:69"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:70" class="idref" href="#l<sub>2</sub>:70"><span class="id" title="binder">l<sub>2</sub></span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:68"><span class="id" title="variable">X</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#length"><span class="id" title="definition">length</span></a> (<a class="idref" href="Poly.html#l<sub>1</sub>:69"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Poly.html#l<sub>2</sub>:70"><span class="id" title="variable">l<sub>2</sub></span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#length"><span class="id" title="definition">length</span></a> <a class="idref" href="Poly.html#l<sub>1</sub>:69"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Poly.html#length"><span class="id" title="definition">length</span></a> <a class="idref" href="Poly.html#l<sub>2</sub>:70"><span class="id" title="variable">l<sub>2</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab111"></a><h4 class="section">Exercise: 2 stars, standard, optional (more_poly_exercises)</h4>
 Here are some slightly more interesting ones... 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="rev_app_distr" class="idref" href="#rev_app_distr"><span class="id" title="lemma">rev_app_distr</span></a>: <span class="id" title="keyword">∀</span> <a id="X:71" class="idref" href="#X:71"><span class="id" title="binder">X</span></a> (<a id="l<sub>1</sub>:72" class="idref" href="#l<sub>1</sub>:72"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:73" class="idref" href="#l<sub>2</sub>:73"><span class="id" title="binder">l<sub>2</sub></span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:71"><span class="id" title="variable">X</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="Poly.html#l<sub>1</sub>:72"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Poly.html#l<sub>2</sub>:73"><span class="id" title="variable">l<sub>2</sub></span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Poly.html#l<sub>2</sub>:73"><span class="id" title="variable">l<sub>2</sub></span></a> <a class="idref" href="Poly.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Poly.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Poly.html#l<sub>1</sub>:72"><span class="id" title="variable">l<sub>1</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="rev_involutive" class="idref" href="#rev_involutive"><span class="id" title="lemma">rev_involutive</span></a> : <span class="id" title="keyword">∀</span> <a id="X:74" class="idref" href="#X:74"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>, <span class="id" title="keyword">∀</span> <a id="l:75" class="idref" href="#l:75"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:74"><span class="id" title="variable">X</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="Poly.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Poly.html#l:75"><span class="id" title="variable">l</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#l:75"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab112"></a><h2 class="section">Polymorphic Pairs</h2>

<div class="paragraph"> </div>

 Following the same pattern, the definition for pairs of
    numbers that we gave in the last chapter can be generalized to
    <i>polymorphic pairs</i>, often called <i>products</i>: 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="prod" class="idref" href="#prod"><span class="id" title="inductive">prod</span></a> (<a id="X:76" class="idref" href="#X:76"><span class="id" title="binder">X</span></a> <a id="Y:77" class="idref" href="#Y:77"><span class="id" title="binder">Y</span></a> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/>
| <a id="pair" class="idref" href="#pair"><span class="id" title="constructor">pair</span></a> (<a id="x:80" class="idref" href="#x:80"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#X:76"><span class="id" title="variable">X</span></a>) (<a id="y:81" class="idref" href="#y:81"><span class="id" title="binder">y</span></a> : <a class="idref" href="Poly.html#Y:77"><span class="id" title="variable">Y</span></a>).<br/><hr class='doublespaceincode'/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Poly.html#pair"><span class="id" title="constructor">pair</span></a> {<span class="id" title="var">X</span>} {<span class="id" title="var">Y</span>}.<br/>
</div>

<div class="doc">
As with lists, we make the type arguments implicit and define the
    familiar concrete notation. 
</div>
<div class="code">

<span class="id" title="keyword">Notation</span> <a id="62264328926d76449e4f268ee9289ca<sub>9</sub>" class="idref" href="#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">&quot;</span></a>( x , y )" := (<a class="idref" href="Poly.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>).<br/>
</div>

<div class="doc">
We can also use the <span class="inlinecode"><span class="id" title="keyword">Notation</span></span> mechanism to define the standard
    notation for product <i>types</i>: 
</div>
<div class="code">

<span class="id" title="keyword">Notation</span> <a id="11c698c8685bb8ab1cf725545c085ac<sub>4</sub>" class="idref" href="#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">&quot;</span></a>X * Y" := (<a class="idref" href="Poly.html#prod"><span class="id" title="inductive">prod</span></a> <span class="id" title="var">X</span> <span class="id" title="var">Y</span>) : <span class="id" title="var">type_scope</span>.<br/>
</div>

<div class="doc">
(The annotation <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">type_scope</span></span> tells Coq that this abbreviation
    should only be used when parsing types, not when parsing
    expressions.  This avoids a clash with the multiplication
    symbol.) 
<div class="paragraph"> </div>

 It is easy at first to get <span class="inlinecode">(<span class="id" title="var">x</span>,<span class="id" title="var">y</span>)</span> and <span class="inlinecode"><span class="id" title="var">X</span>×<span class="id" title="var">Y</span></span> confused.
    Remember that <span class="inlinecode">(<span class="id" title="var">x</span>,<span class="id" title="var">y</span>)</span> is a <i>value</i> built from two other values,
    while <span class="inlinecode"><span class="id" title="var">X</span>×<span class="id" title="var">Y</span></span> is a <i>type</i> built from two other types.  If <span class="inlinecode"><span class="id" title="var">x</span></span> has
    type <span class="inlinecode"><span class="id" title="var">X</span></span> and <span class="inlinecode"><span class="id" title="var">y</span></span> has type <span class="inlinecode"><span class="id" title="var">Y</span></span>, then <span class="inlinecode">(<span class="id" title="var">x</span>,<span class="id" title="var">y</span>)</span> has type <span class="inlinecode"><span class="id" title="var">X</span>×<span class="id" title="var">Y</span></span>. 
<div class="paragraph"> </div>

 The first and second projection functions now look pretty
    much as they would in any functional programming language. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="fst" class="idref" href="#fst"><span class="id" title="definition">fst</span></a> {<a id="X:82" class="idref" href="#X:82"><span class="id" title="binder">X</span></a> <a id="Y:83" class="idref" href="#Y:83"><span class="id" title="binder">Y</span></a> : <span class="id" title="keyword">Type</span>} (<a id="p:84" class="idref" href="#p:84"><span class="id" title="binder">p</span></a> : <a class="idref" href="Poly.html#X:82"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Poly.html#Y:83"><span class="id" title="variable">Y</span></a>) : <a class="idref" href="Poly.html#X:82"><span class="id" title="variable">X</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#p:84"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a> <span class="id" title="var">y</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a> ⇒ <span class="id" title="var">x</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="snd" class="idref" href="#snd"><span class="id" title="definition">snd</span></a> {<a id="X:86" class="idref" href="#X:86"><span class="id" title="binder">X</span></a> <a id="Y:87" class="idref" href="#Y:87"><span class="id" title="binder">Y</span></a> : <span class="id" title="keyword">Type</span>} (<a id="p:88" class="idref" href="#p:88"><span class="id" title="binder">p</span></a> : <a class="idref" href="Poly.html#X:86"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Poly.html#Y:87"><span class="id" title="variable">Y</span></a>) : <a class="idref" href="Poly.html#Y:87"><span class="id" title="variable">Y</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#p:88"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a> <span class="id" title="var">y</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a> ⇒ <span class="id" title="var">y</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
The following function takes two lists and combines them
    into a list of pairs.  In other functional languages, it is often
    called <span class="inlinecode"><span class="id" title="var">zip</span></span>; we call it <span class="inlinecode"><span class="id" title="var">combine</span></span> for consistency with Coq's
    standard library. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="combine" class="idref" href="#combine"><span class="id" title="definition">combine</span></a> {<a id="X:90" class="idref" href="#X:90"><span class="id" title="binder">X</span></a> <a id="Y:91" class="idref" href="#Y:91"><span class="id" title="binder">Y</span></a> : <span class="id" title="keyword">Type</span>} (<a id="lx:92" class="idref" href="#lx:92"><span class="id" title="binder">lx</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:90"><span class="id" title="variable">X</span></a>) (<a id="ly:93" class="idref" href="#ly:93"><span class="id" title="binder">ly</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#Y:91"><span class="id" title="variable">Y</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> (<a class="idref" href="Poly.html#X:90"><span class="id" title="variable">X</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="Poly.html#Y:91"><span class="id" title="variable">Y</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#lx:92"><span class="id" title="variable">lx</span></a>, <a class="idref" href="Poly.html#ly:93"><span class="id" title="variable">ly</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a>, <span class="id" title="var">_</span> ⇒ <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">_</span>, <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a> ⇒ <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">x</span> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">tx</span>, <span class="id" title="var">y</span> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">ty</span> ⇒ <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a> <span class="id" title="var">y</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#combine:94"><span class="id" title="definition">combine</span></a> <span class="id" title="var">tx</span> <span class="id" title="var">ty</span><a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
<a id="lab113"></a><h4 class="section">Exercise: 1 star, standard, optional (combine_checks)</h4>
 Try answering the following questions on paper and
    checking your answers in Coq:
<ul class="doclist">
<li> What is the type of <span class="inlinecode"><span class="id" title="var">combine</span></span> (i.e., what does <span class="inlinecode"><span class="id" title="keyword">Check</span></span>
      <span class="inlinecode">@<span class="id" title="var">combine</span></span> print?)

</li>
<li> What does
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Compute</span> (<span class="id" title="var">combine</span> [1;2] [<span class="id" title="var">false</span>;<span class="id" title="var">false</span>;<span class="id" title="var">true</span>;<span class="id" title="var">true</span>]).
</span>      print? 
</li>
</ul>
 <font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a id="lab114"></a><h4 class="section">Exercise: 2 stars, standard, especially useful (split)</h4>
 The function <span class="inlinecode"><span class="id" title="tactic">split</span></span> is the right inverse of <span class="inlinecode"><span class="id" title="var">combine</span></span>: it takes a
    list of pairs and returns a pair of lists.  In many functional
    languages, it is called <span class="inlinecode"><span class="id" title="var">unzip</span></span>.

<div class="paragraph"> </div>

    Fill in the definition of <span class="inlinecode"><span class="id" title="tactic">split</span></span> below.  Make sure it passes the
    given unit test. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="split" class="idref" href="#split"><span class="id" title="definition">split</span></a> {<a id="X:97" class="idref" href="#X:97"><span class="id" title="binder">X</span></a> <a id="Y:98" class="idref" href="#Y:98"><span class="id" title="binder">Y</span></a> : <span class="id" title="keyword">Type</span>} (<a id="l:99" class="idref" href="#l:99"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> (<a class="idref" href="Poly.html#X:97"><span class="id" title="variable">X</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="Poly.html#Y:98"><span class="id" title="variable">Y</span></a>)) : <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:97"><span class="id" title="variable">X</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#Y:98"><span class="id" title="variable">Y</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_split" class="idref" href="#test_split"><span class="id" title="definition">test_split</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#split"><span class="id" title="axiom">split</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a>1<a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a>2<a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab115"></a><h2 class="section">Polymorphic Options</h2>

<div class="paragraph"> </div>

 Our last polymorphic type for now is <i>polymorphic options</i>,
    which generalize <span class="inlinecode"><span class="id" title="var">natoption</span></span> from the previous chapter.  (We put
    the definition inside a module because the standard library
    already defines <span class="inlinecode"><span class="id" title="var">option</span></span> and it's this one that we want to use
    below.) 
</div>
<div class="code">

<span class="id" title="keyword">Module</span> <a id="OptionPlayground" class="idref" href="#OptionPlayground"><span class="id" title="module">OptionPlayground</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="OptionPlayground.option" class="idref" href="#OptionPlayground.option"><span class="id" title="inductive">option</span></a> (<a id="X:101" class="idref" href="#X:101"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="OptionPlayground.Some" class="idref" href="#OptionPlayground.Some"><span class="id" title="constructor">Some</span></a> (<a id="x:104" class="idref" href="#x:104"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#X:101"><span class="id" title="variable">X</span></a>)<br/>
&nbsp;&nbsp;| <a id="OptionPlayground.None" class="idref" href="#OptionPlayground.None"><span class="id" title="constructor">None</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Poly.html#OptionPlayground.Some"><span class="id" title="constructor">Some</span></a> {<span class="id" title="var">X</span>}.<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Poly.html#OptionPlayground.None"><span class="id" title="constructor">None</span></a> {<span class="id" title="var">X</span>}.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">End</span> <a class="idref" href="Poly.html#OptionPlayground"><span class="id" title="module">OptionPlayground</span></a>.<br/>
</div>

<div class="doc">
We can now rewrite the <span class="inlinecode"><span class="id" title="var">nth_error</span></span> function so that it works
    with any type of lists. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="nth_error" class="idref" href="#nth_error"><span class="id" title="definition">nth_error</span></a> {<a id="X:105" class="idref" href="#X:105"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>} (<a id="l:106" class="idref" href="#l:106"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:105"><span class="id" title="variable">X</span></a>) (<a id="n:107" class="idref" href="#n:107"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="Poly.html#X:105"><span class="id" title="variable">X</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#l:106"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">a</span> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">l'</span> ⇒ <span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#n:107"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">a</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">n'</span> ⇒ <a class="idref" href="Poly.html#nth_error:108"><span class="id" title="definition">nth_error</span></a> <span class="id" title="var">l'</span> <span class="id" title="var">n'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_nth_error1" class="idref" href="#test_nth_error1"><span class="id" title="definition">test_nth_error1</span></a> : <a class="idref" href="Poly.html#nth_error"><span class="id" title="definition">nth_error</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>6<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>7<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> 4.<br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
<span class="id" title="keyword">Example</span> <a id="test_nth_error2" class="idref" href="#test_nth_error2"><span class="id" title="definition">test_nth_error2</span></a> : <a class="idref" href="Poly.html#nth_error"><span class="id" title="definition">nth_error</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];[</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]]</span></a> 1 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
<span class="id" title="keyword">Example</span> <a id="test_nth_error3" class="idref" href="#test_nth_error3"><span class="id" title="definition">test_nth_error3</span></a> : <a class="idref" href="Poly.html#nth_error"><span class="id" title="definition">nth_error</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> 2 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<div class="togglescript" id="proofcontrol8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')"><span class="show"></span></div>
<div class="proofscript" id="proof8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab116"></a><h4 class="section">Exercise: 1 star, standard, optional (hd_error_poly)</h4>
 Complete the definition of a polymorphic version of the
    <span class="inlinecode"><span class="id" title="var">hd_error</span></span> function from the last chapter. Be sure that it
    passes the unit tests below. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="hd_error" class="idref" href="#hd_error"><span class="id" title="definition">hd_error</span></a> {<a id="X:111" class="idref" href="#X:111"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>} (<a id="l:112" class="idref" href="#l:112"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:111"><span class="id" title="variable">X</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="Poly.html#X:111"><span class="id" title="variable">X</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/>
</div>

<div class="doc">
Once again, to force the implicit arguments to be explicit,
    we can use <span class="inlinecode">@</span> before the name of the function. 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> @<a class="idref" href="Poly.html#hd_error"><span class="id" title="axiom">hd_error</span></a> : <span class="id" title="keyword">∀</span> <a id="X:113" class="idref" href="#X:113"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>, <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:113"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="Poly.html#X:113"><span class="id" title="variable">X</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_hd_error1" class="idref" href="#test_hd_error1"><span class="id" title="definition">test_hd_error1</span></a> : <a class="idref" href="Poly.html#hd_error"><span class="id" title="axiom">hd_error</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> 1.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="test_hd_error2" class="idref" href="#test_hd_error2"><span class="id" title="definition">test_hd_error2</span></a> : <a class="idref" href="Poly.html#hd_error"><span class="id" title="axiom">hd_error</span></a>  <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];[</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]]</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab117"></a><h1 class="section">Functions as Data</h1>

<div class="paragraph"> </div>

 Like most modern programming languages -- especially other
    "functional" languages, including OCaml, Haskell, Racket, Scala,
    Clojure, etc. -- Coq treats functions as first-class citizens,
    allowing them to be passed as arguments to other functions,
    returned as results, stored in data structures, etc. 
</div>

<div class="doc">
<a id="lab118"></a><h2 class="section">Higher-Order Functions</h2>

<div class="paragraph"> </div>

 Functions that manipulate other functions are often called
    <i>higher-order</i> functions.  Here's a simple one: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="doit3times" class="idref" href="#doit3times"><span class="id" title="definition">doit3times</span></a> {<a id="X:114" class="idref" href="#X:114"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>} (<a id="f:115" class="idref" href="#f:115"><span class="id" title="binder">f</span></a> : <a class="idref" href="Poly.html#X:114"><span class="id" title="variable">X</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Poly.html#X:114"><span class="id" title="variable">X</span></a>) (<a id="n:116" class="idref" href="#n:116"><span class="id" title="binder">n</span></a> : <a class="idref" href="Poly.html#X:114"><span class="id" title="variable">X</span></a>) : <a class="idref" href="Poly.html#X:114"><span class="id" title="variable">X</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#f:115"><span class="id" title="variable">f</span></a> (<a class="idref" href="Poly.html#f:115"><span class="id" title="variable">f</span></a> (<a class="idref" href="Poly.html#f:115"><span class="id" title="variable">f</span></a> <a class="idref" href="Poly.html#n:116"><span class="id" title="variable">n</span></a>)).<br/>
</div>

<div class="doc">
The argument <span class="inlinecode"><span class="id" title="var">f</span></span> here is itself a function (from <span class="inlinecode"><span class="id" title="var">X</span></span> to
    <span class="inlinecode"><span class="id" title="var">X</span></span>); the body of <span class="inlinecode"><span class="id" title="var">doit3times</span></span> applies <span class="inlinecode"><span class="id" title="var">f</span></span> three times to some
    value <span class="inlinecode"><span class="id" title="var">n</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> @<a class="idref" href="Poly.html#doit3times"><span class="id" title="definition">doit3times</span></a> : <span class="id" title="keyword">∀</span> <a id="X:117" class="idref" href="#X:117"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>, <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#X:117"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#X:117"><span class="id" title="variable">X</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#X:117"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#X:117"><span class="id" title="variable">X</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_doit3times" class="idref" href="#test_doit3times"><span class="id" title="definition">test_doit3times</span></a>: <a class="idref" href="Poly.html#doit3times"><span class="id" title="definition">doit3times</span></a> <a class="idref" href="Basics.html#minustwo"><span class="id" title="definition">minustwo</span></a> 9 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 3.<br/>
<div class="togglescript" id="proofcontrol9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')"><span class="show"></span></div>
<div class="proofscript" id="proof9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Example</span> <a id="test_doit3times'" class="idref" href="#test_doit3times'"><span class="id" title="definition">test_doit3times'</span></a>: <a class="idref" href="Poly.html#doit3times"><span class="id" title="definition">doit3times</span></a> <a class="idref" href="Basics.html#negb"><span class="id" title="definition">negb</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<div class="togglescript" id="proofcontrol10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')"><span class="show"></span></div>
<div class="proofscript" id="proof10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab119"></a><h2 class="section">Filter</h2>

<div class="paragraph"> </div>

 Here is a more useful higher-order function, taking a list
    of <span class="inlinecode"><span class="id" title="var">X</span></span>s and a <i>predicate</i> on <span class="inlinecode"><span class="id" title="var">X</span></span> (a function from <span class="inlinecode"><span class="id" title="var">X</span></span> to <span class="inlinecode"><span class="id" title="var">bool</span></span>)
    and "filtering" the list, returning a new list containing just
    those elements for which the predicate returns <span class="inlinecode"><span class="id" title="var">true</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="filter" class="idref" href="#filter"><span class="id" title="definition">filter</span></a> {<a id="X:118" class="idref" href="#X:118"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>} (<a id="test:119" class="idref" href="#test:119"><span class="id" title="binder">test</span></a>: <a class="idref" href="Poly.html#X:118"><span class="id" title="variable">X</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>) (<a id="l:120" class="idref" href="#l:120"><span class="id" title="binder">l</span></a>:<a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:118"><span class="id" title="variable">X</span></a>) : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:118"><span class="id" title="variable">X</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#l:120"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a> ⇒ <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">h</span> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">t</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="Poly.html#test:119"><span class="id" title="variable">test</span></a> <span class="id" title="var">h</span> <span class="id" title="keyword">then</span> <span class="id" title="var">h</span> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#filter:121"><span class="id" title="definition">filter</span></a> <a class="idref" href="Poly.html#test:119"><span class="id" title="variable">test</span></a> <span class="id" title="var">t</span><a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="Poly.html#filter:121"><span class="id" title="definition">filter</span></a> <a class="idref" href="Poly.html#test:119"><span class="id" title="variable">test</span></a> <span class="id" title="var">t</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
For example, if we apply <span class="inlinecode"><span class="id" title="var">filter</span></span> to the predicate <span class="inlinecode"><span class="id" title="var">even</span></span>
    and a list of numbers <span class="inlinecode"><span class="id" title="var">l</span></span>, it returns a list containing just the
    even members of <span class="inlinecode"><span class="id" title="var">l</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Example</span> <a id="test_filter1" class="idref" href="#test_filter1"><span class="id" title="definition">test_filter1</span></a>: <a class="idref" href="Poly.html#filter"><span class="id" title="definition">filter</span></a> <a class="idref" href="Basics.html#even"><span class="id" title="definition">even</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<div class="togglescript" id="proofcontrol11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')"><span class="show"></span></div>
<div class="proofscript" id="proof11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Definition</span> <a id="length_is_1" class="idref" href="#length_is_1"><span class="id" title="definition">length_is_1</span></a> {<a id="X:123" class="idref" href="#X:123"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>} (<a id="l:124" class="idref" href="#l:124"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:123"><span class="id" title="variable">X</span></a>) : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#length"><span class="id" title="definition">length</span></a> <a class="idref" href="Poly.html#l:124"><span class="id" title="variable">l</span></a><a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 1.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_filter2" class="idref" href="#test_filter2"><span class="id" title="definition">test_filter2</span></a>:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#filter"><span class="id" title="definition">filter</span></a> <a class="idref" href="Poly.html#length_is_1"><span class="id" title="definition">length_is_1</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>6<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>7<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>8<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>8<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<div class="togglescript" id="proofcontrol12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')"><span class="show"></span></div>
<div class="proofscript" id="proof12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
We can use <span class="inlinecode"><span class="id" title="var">filter</span></span> to give a concise version of the
    <span class="inlinecode"><span class="id" title="var">countoddmembers</span></span> function from the <a href="Lists.html"><span class="inlineref">Lists</span></a> chapter. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="countoddmembers'" class="idref" href="#countoddmembers'"><span class="id" title="definition">countoddmembers'</span></a> (<a id="l:125" class="idref" href="#l:125"><span class="id" title="binder">l</span></a>:<a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#length"><span class="id" title="definition">length</span></a> (<a class="idref" href="Poly.html#filter"><span class="id" title="definition">filter</span></a> <a class="idref" href="Basics.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="Poly.html#l:125"><span class="id" title="variable">l</span></a>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_countoddmembers'1" class="idref" href="#test_countoddmembers'1"><span class="id" title="definition">test_countoddmembers'1</span></a>:   <a class="idref" href="Poly.html#countoddmembers'"><span class="id" title="definition">countoddmembers'</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 4.<br/>
<div class="togglescript" id="proofcontrol13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')"><span class="show"></span></div>
<div class="proofscript" id="proof13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
<span class="id" title="keyword">Example</span> <a id="test_countoddmembers'2" class="idref" href="#test_countoddmembers'2"><span class="id" title="definition">test_countoddmembers'2</span></a>:   <a class="idref" href="Poly.html#countoddmembers'"><span class="id" title="definition">countoddmembers'</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
<div class="togglescript" id="proofcontrol14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')"><span class="show"></span></div>
<div class="proofscript" id="proof14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
<span class="id" title="keyword">Example</span> <a id="test_countoddmembers'3" class="idref" href="#test_countoddmembers'3"><span class="id" title="definition">test_countoddmembers'3</span></a>:   <a class="idref" href="Poly.html#countoddmembers'"><span class="id" title="definition">countoddmembers'</span></a> <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
<div class="togglescript" id="proofcontrol15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')"><span class="show"></span></div>
<div class="proofscript" id="proof15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab120"></a><h2 class="section">Anonymous Functions</h2>

<div class="paragraph"> </div>

 It is arguably a little sad, in the example just above, to
    be forced to define the function <span class="inlinecode"><span class="id" title="var">length_is_1</span></span> and give it a name
    just to be able to pass it as an argument to <span class="inlinecode"><span class="id" title="var">filter</span></span>, since we
    will probably never use it again.  Moreover, this is not an
    isolated example: when using higher-order functions, we often want
    to pass as arguments "one-off" functions that we will never use
    again; having to give each of these functions a name would be
    tedious.

<div class="paragraph"> </div>

    Fortunately, there is a better way.  We can construct a function
    "on the fly" without declaring it at the top level or giving it a
    name. 
</div>
<div class="code">

<span class="id" title="keyword">Example</span> <a id="test_anon_fun'" class="idref" href="#test_anon_fun'"><span class="id" title="definition">test_anon_fun'</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#doit3times"><span class="id" title="definition">doit3times</span></a> (<span class="id" title="keyword">fun</span> <a id="n:126" class="idref" href="#n:126"><span class="id" title="binder">n</span></a> ⇒ <a class="idref" href="Poly.html#n:126"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Poly.html#n:126"><span class="id" title="variable">n</span></a>) 2 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 256.<br/>
<div class="togglescript" id="proofcontrol16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')"><span class="show"></span></div>
<div class="proofscript" id="proof16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
The expression <span class="inlinecode">(<span class="id" title="keyword">fun</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">⇒</span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">×</span> <span class="inlinecode"><span class="id" title="var">n</span>)</span> can be read as "the function
    that, given a number <span class="inlinecode"><span class="id" title="var">n</span></span>, yields <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">×</span> <span class="inlinecode"><span class="id" title="var">n</span></span>." 
<div class="paragraph"> </div>

 Here is the <span class="inlinecode"><span class="id" title="var">filter</span></span> example, rewritten to use an anonymous
    function. 
</div>
<div class="code">

<span class="id" title="keyword">Example</span> <a id="test_filter2'" class="idref" href="#test_filter2'"><span class="id" title="definition">test_filter2'</span></a>:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#filter"><span class="id" title="definition">filter</span></a> (<span class="id" title="keyword">fun</span> <a id="l:127" class="idref" href="#l:127"><span class="id" title="binder">l</span></a> ⇒ <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#length"><span class="id" title="definition">length</span></a> <a class="idref" href="Poly.html#l:127"><span class="id" title="variable">l</span></a><a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 1)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>6<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>7<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>8<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>8<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<div class="togglescript" id="proofcontrol17" onclick="toggleDisplay('proof17');toggleDisplay('proofcontrol17')"><span class="show"></span></div>
<div class="proofscript" id="proof17" onclick="toggleDisplay('proof17');toggleDisplay('proofcontrol17')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab121"></a><h4 class="section">Exercise: 2 stars, standard (filter_even_gt<sub>7</sub>)</h4>
 Use <span class="inlinecode"><span class="id" title="var">filter</span></span> (instead of <span class="inlinecode"><span class="id" title="keyword">Fixpoint</span></span>) to write a Coq function
    <span class="inlinecode"><span class="id" title="var">filter_even_gt<sub>7</sub></span></span> that takes a list of natural numbers as input
    and returns a list of just those that are even and greater than
    7. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="filter_even_gt<sub>7</sub>" class="idref" href="#filter_even_gt<sub>7</sub>"><span class="id" title="definition">filter_even_gt<sub>7</sub></span></a> (<a id="l:128" class="idref" href="#l:128"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_filter_even_gt7_1" class="idref" href="#test_filter_even_gt7_1"><span class="id" title="definition">test_filter_even_gt7_1</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#filter_even_gt<sub>7</sub>"><span class="id" title="axiom">filter_even_gt<sub>7</sub></span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>6<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>9<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>10<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>12<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>8<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>10<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>12<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>8<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_filter_even_gt7_2" class="idref" href="#test_filter_even_gt7_2"><span class="id" title="definition">test_filter_even_gt7_2</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#filter_even_gt<sub>7</sub>"><span class="id" title="axiom">filter_even_gt<sub>7</sub></span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>6<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>19<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>129<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab122"></a><h4 class="section">Exercise: 3 stars, standard (partition)</h4>
 Use <span class="inlinecode"><span class="id" title="var">filter</span></span> to write a Coq function <span class="inlinecode"><span class="id" title="var">partition</span></span>:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">partition</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">X</span> : <span class="id" title="keyword">Type</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">X</span> → <span class="id" title="var">bool</span>) → <span class="id" title="var">list</span> <span class="id" title="var">X</span> → <span class="id" title="var">list</span> <span class="id" title="var">X</span> × <span class="id" title="var">list</span> <span class="id" title="var">X</span>
</span>   Given a set <span class="inlinecode"><span class="id" title="var">X</span></span>, a predicate of type <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">bool</span></span> and a <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span>,
   <span class="inlinecode"><span class="id" title="var">partition</span></span> should return a pair of lists.  The first member of the
   pair is the sublist of the original list containing the elements
   that satisfy the test, and the second is the sublist containing
   those that fail the test.  The order of elements in the two
   sublists should be the same as their order in the original list. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="partition" class="idref" href="#partition"><span class="id" title="definition">partition</span></a> {<a id="X:129" class="idref" href="#X:129"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="test:130" class="idref" href="#test:130"><span class="id" title="binder">test</span></a> : <a class="idref" href="Poly.html#X:129"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="l:131" class="idref" href="#l:131"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:129"><span class="id" title="variable">X</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:129"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:129"><span class="id" title="variable">X</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_partition1" class="idref" href="#test_partition1"><span class="id" title="definition">test_partition1</span></a>: <a class="idref" href="Poly.html#partition"><span class="id" title="axiom">partition</span></a> <a class="idref" href="Basics.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="test_partition2" class="idref" href="#test_partition2"><span class="id" title="definition">test_partition2</span></a>: <a class="idref" href="Poly.html#partition"><span class="id" title="axiom">partition</span></a> (<span class="id" title="keyword">fun</span> <a id="x:132" class="idref" href="#x:132"><span class="id" title="binder">x</span></a> ⇒ <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>) <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>9<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>9<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab123"></a><h2 class="section">Map</h2>

<div class="paragraph"> </div>

 Another handy higher-order function is called <span class="inlinecode"><span class="id" title="var">map</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="map" class="idref" href="#map"><span class="id" title="definition">map</span></a> {<a id="X:133" class="idref" href="#X:133"><span class="id" title="binder">X</span></a> <a id="Y:134" class="idref" href="#Y:134"><span class="id" title="binder">Y</span></a> : <span class="id" title="keyword">Type</span>} (<a id="f:135" class="idref" href="#f:135"><span class="id" title="binder">f</span></a> : <a class="idref" href="Poly.html#X:133"><span class="id" title="variable">X</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Poly.html#Y:134"><span class="id" title="variable">Y</span></a>) (<a id="l:136" class="idref" href="#l:136"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:133"><span class="id" title="variable">X</span></a>) : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#Y:134"><span class="id" title="variable">Y</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#l:136"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a>     ⇒ <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">h</span> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">t</span> ⇒ <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#f:135"><span class="id" title="variable">f</span></a> <span class="id" title="var">h</span><a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#map:137"><span class="id" title="definition">map</span></a> <a class="idref" href="Poly.html#f:135"><span class="id" title="variable">f</span></a> <span class="id" title="var">t</span><a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
It takes a function <span class="inlinecode"><span class="id" title="var">f</span></span> and a list <span class="inlinecode"></span> <span class="inlinecode"><span class="id" title="var">l</span></span> <span class="inlinecode">=</span> <span class="inlinecode">[<span class="id" title="var">n<sub>1</sub></span>,</span> <span class="inlinecode"><span class="id" title="var">n<sub>2</sub></span>,</span> <span class="inlinecode"><span class="id" title="var">n<sub>3</sub></span>,</span> <span class="inlinecode">...]</span> <span class="inlinecode"></span>
    and returns the list <span class="inlinecode"></span> <span class="inlinecode">[<span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">n<sub>1</sub></span>,</span> <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">n<sub>2</sub></span>,</span> <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">n<sub>3</sub></span>,...]</span> <span class="inlinecode"></span>, where <span class="inlinecode"><span class="id" title="var">f</span></span> has
    been applied to each element of <span class="inlinecode"><span class="id" title="var">l</span></span> in turn.  For example: 
</div>
<div class="code">

<span class="id" title="keyword">Example</span> <a id="test_map1" class="idref" href="#test_map1"><span class="id" title="definition">test_map1</span></a>: <a class="idref" href="Poly.html#map"><span class="id" title="definition">map</span></a> (<span class="id" title="keyword">fun</span> <a id="x:139" class="idref" href="#x:139"><span class="id" title="binder">x</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> 3 <a class="idref" href="Poly.html#x:139"><span class="id" title="variable">x</span></a>) <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<div class="togglescript" id="proofcontrol18" onclick="toggleDisplay('proof18');toggleDisplay('proofcontrol18')"><span class="show"></span></div>
<div class="proofscript" id="proof18" onclick="toggleDisplay('proof18');toggleDisplay('proofcontrol18')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
The element types of the input and output lists need not be
    the same, since <span class="inlinecode"><span class="id" title="var">map</span></span> takes <i>two</i> type arguments, <span class="inlinecode"><span class="id" title="var">X</span></span> and <span class="inlinecode"><span class="id" title="var">Y</span></span>; it
    can thus be applied to a list of numbers and a function from
    numbers to booleans to yield a list of booleans: 
</div>
<div class="code">

<span class="id" title="keyword">Example</span> <a id="test_map2" class="idref" href="#test_map2"><span class="id" title="definition">test_map2</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="Basics.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<div class="togglescript" id="proofcontrol19" onclick="toggleDisplay('proof19');toggleDisplay('proofcontrol19')"><span class="show"></span></div>
<div class="proofscript" id="proof19" onclick="toggleDisplay('proof19');toggleDisplay('proofcontrol19')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
It can even be applied to a list of numbers and
    a function from numbers to <i>lists</i> of booleans to
    yield a <i>list of lists</i> of booleans: 
</div>
<div class="code">

<span class="id" title="keyword">Example</span> <a id="test_map3" class="idref" href="#test_map3"><span class="id" title="definition">test_map3</span></a>:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#map"><span class="id" title="definition">map</span></a> (<span class="id" title="keyword">fun</span> <a id="n:140" class="idref" href="#n:140"><span class="id" title="binder">n</span></a> ⇒ <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Basics.html#even"><span class="id" title="definition">even</span></a> <a class="idref" href="Poly.html#n:140"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="Poly.html#n:140"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>) <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[[</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];[</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];[</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];[</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]]</span></a>.<br/>
<div class="togglescript" id="proofcontrol20" onclick="toggleDisplay('proof20');toggleDisplay('proofcontrol20')"><span class="show"></span></div>
<div class="proofscript" id="proof20" onclick="toggleDisplay('proof20');toggleDisplay('proofcontrol20')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab124"></a><h3 class="section">Exercises</h3>

<div class="paragraph"> </div>

<a id="lab125"></a><h4 class="section">Exercise: 3 stars, standard (map_rev)</h4>
 Show that <span class="inlinecode"><span class="id" title="var">map</span></span> and <span class="inlinecode"><span class="id" title="var">rev</span></span> commute.  You may need to define an
    auxiliary lemma. 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="map_rev" class="idref" href="#map_rev"><span class="id" title="lemma">map_rev</span></a> : <span class="id" title="keyword">∀</span> (<a id="X:141" class="idref" href="#X:141"><span class="id" title="binder">X</span></a> <a id="Y:142" class="idref" href="#Y:142"><span class="id" title="binder">Y</span></a> : <span class="id" title="keyword">Type</span>) (<a id="f:143" class="idref" href="#f:143"><span class="id" title="binder">f</span></a> : <a class="idref" href="Poly.html#X:141"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#Y:142"><span class="id" title="variable">Y</span></a>) (<a id="l:144" class="idref" href="#l:144"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:141"><span class="id" title="variable">X</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="Poly.html#f:143"><span class="id" title="variable">f</span></a> (<a class="idref" href="Poly.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Poly.html#l:144"><span class="id" title="variable">l</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="Poly.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="Poly.html#f:143"><span class="id" title="variable">f</span></a> <a class="idref" href="Poly.html#l:144"><span class="id" title="variable">l</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab126"></a><h4 class="section">Exercise: 2 stars, standard, especially useful (flat_map)</h4>
 The function <span class="inlinecode"><span class="id" title="var">map</span></span> maps a <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> to a <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">Y</span></span> using a function
    of type <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">Y</span></span>.  We can define a similar function, <span class="inlinecode"><span class="id" title="var">flat_map</span></span>,
    which maps a <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> to a <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">Y</span></span> using a function <span class="inlinecode"><span class="id" title="var">f</span></span> of type
    <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">list</span></span> <span class="inlinecode"><span class="id" title="var">Y</span></span>.  Your definition should work by 'flattening' the
    results of <span class="inlinecode"><span class="id" title="var">f</span></span>, like so:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">flat_map</span> (<span class="id" title="keyword">fun</span> <span class="id" title="var">n</span> ⇒ [<span class="id" title="var">n</span>;<span class="id" title="var">n</span>+1;<span class="id" title="var">n</span>+2]) [1;5;10]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;= [1; 2; 3; 5; 6; 7; 10; 11; 12].
</span>
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="flat_map" class="idref" href="#flat_map"><span class="id" title="definition">flat_map</span></a> {<a id="X:145" class="idref" href="#X:145"><span class="id" title="binder">X</span></a> <a id="Y:146" class="idref" href="#Y:146"><span class="id" title="binder">Y</span></a>: <span class="id" title="keyword">Type</span>} (<a id="f:147" class="idref" href="#f:147"><span class="id" title="binder">f</span></a>: <a class="idref" href="Poly.html#X:145"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#Y:146"><span class="id" title="variable">Y</span></a>) (<a id="l:148" class="idref" href="#l:148"><span class="id" title="binder">l</span></a>: <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:145"><span class="id" title="variable">X</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#Y:146"><span class="id" title="variable">Y</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_flat_map1" class="idref" href="#test_flat_map1"><span class="id" title="definition">test_flat_map1</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#flat_map"><span class="id" title="axiom">flat_map</span></a> (<span class="id" title="keyword">fun</span> <a id="n:150" class="idref" href="#n:150"><span class="id" title="binder">n</span></a> ⇒ <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Poly.html#n:150"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Poly.html#n:150"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Poly.html#n:150"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>) <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> 4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 Lists are not the only inductive type for which <span class="inlinecode"><span class="id" title="var">map</span></span> makes sense.
    Here is a <span class="inlinecode"><span class="id" title="var">map</span></span> for the <span class="inlinecode"><span class="id" title="var">option</span></span> type: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="option_map" class="idref" href="#option_map"><span class="id" title="definition">option_map</span></a> {<a id="X:151" class="idref" href="#X:151"><span class="id" title="binder">X</span></a> <a id="Y:152" class="idref" href="#Y:152"><span class="id" title="binder">Y</span></a> : <span class="id" title="keyword">Type</span>} (<a id="f:153" class="idref" href="#f:153"><span class="id" title="binder">f</span></a> : <a class="idref" href="Poly.html#X:151"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#Y:152"><span class="id" title="variable">Y</span></a>) (<a id="xo:154" class="idref" href="#xo:154"><span class="id" title="binder">xo</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="Poly.html#X:151"><span class="id" title="variable">X</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="Poly.html#Y:152"><span class="id" title="variable">Y</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#xo:154"><span class="id" title="variable">xo</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> (<a class="idref" href="Poly.html#f:153"><span class="id" title="variable">f</span></a> <span class="id" title="var">x</span>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
<a id="lab127"></a><h4 class="section">Exercise: 2 stars, standard, optional (implicit_args)</h4>
 The definitions and uses of <span class="inlinecode"><span class="id" title="var">filter</span></span> and <span class="inlinecode"><span class="id" title="var">map</span></span> use implicit
    arguments in many places.  Replace the curly braces around the
    implicit arguments with parentheses, and then fill in explicit
    type parameters where necessary and use Coq to check that you've
    done so correctly.  (This exercise is not to be turned in; it is
    probably easiest to do it on a <i>copy</i> of this file that you can
    throw away afterwards.)
 <font size=-2>&#9744;</font> 
</div>

<div class="doc">
<a id="lab128"></a><h2 class="section">Fold</h2>

<div class="paragraph"> </div>

 An even more powerful higher-order function is called
    <span class="inlinecode"><span class="id" title="tactic">fold</span></span>.  This function is the inspiration for the "<span class="inlinecode"><span class="id" title="var">reduce</span></span>"
    operation that lies at the heart of Google's map/reduce
    distributed programming framework. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="fold" class="idref" href="#fold"><span class="id" title="definition">fold</span></a> {<a id="X:156" class="idref" href="#X:156"><span class="id" title="binder">X</span></a> <a id="Y:157" class="idref" href="#Y:157"><span class="id" title="binder">Y</span></a>: <span class="id" title="keyword">Type</span>} (<a id="f:158" class="idref" href="#f:158"><span class="id" title="binder">f</span></a> : <a class="idref" href="Poly.html#X:156"><span class="id" title="variable">X</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Poly.html#Y:157"><span class="id" title="variable">Y</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Poly.html#Y:157"><span class="id" title="variable">Y</span></a>) (<a id="l:159" class="idref" href="#l:159"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:156"><span class="id" title="variable">X</span></a>) (<a id="b:160" class="idref" href="#b:160"><span class="id" title="binder">b</span></a> : <a class="idref" href="Poly.html#Y:157"><span class="id" title="variable">Y</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="Poly.html#Y:157"><span class="id" title="variable">Y</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Poly.html#l:159"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#nil"><span class="id" title="constructor">nil</span></a> ⇒ <a class="idref" href="Poly.html#b:160"><span class="id" title="variable">b</span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">h</span> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">t</span> ⇒ <a class="idref" href="Poly.html#f:158"><span class="id" title="variable">f</span></a> <span class="id" title="var">h</span> (<a class="idref" href="Poly.html#fold:161"><span class="id" title="definition">fold</span></a> <a class="idref" href="Poly.html#f:158"><span class="id" title="variable">f</span></a> <span class="id" title="var">t</span> <a class="idref" href="Poly.html#b:160"><span class="id" title="variable">b</span></a>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
Intuitively, the behavior of the <span class="inlinecode"><span class="id" title="tactic">fold</span></span> operation is to
    insert a given binary operator <span class="inlinecode"><span class="id" title="var">f</span></span> between every pair of elements
    in a given list.  For example, <span class="inlinecode"></span> <span class="inlinecode"><span class="id" title="tactic">fold</span></span> <span class="inlinecode"><span class="id" title="var">plus</span></span> <span class="inlinecode">[1;2;3;4]</span> <span class="inlinecode"></span> intuitively
    means <span class="inlinecode">1+2+3+4</span>.  To make this precise, we also need a "starting
    element" that serves as the initial second input to <span class="inlinecode"><span class="id" title="var">f</span></span>.  So, for
    example,
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">fold</span> <span class="id" title="var">plus</span> [1;2;3;4] 0
</span>    yields
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;1 + (2 + (3 + (4 + 0))).
</span>    Some more examples: 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> (<a class="idref" href="Poly.html#fold"><span class="id" title="definition">fold</span></a> <a class="idref" href="Basics.html#andb"><span class="id" title="definition">andb</span></a>) : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="fold_example1" class="idref" href="#fold_example1"><span class="id" title="definition">fold_example1</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#fold"><span class="id" title="definition">fold</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> 1 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 24.<br/>
<div class="togglescript" id="proofcontrol21" onclick="toggleDisplay('proof21');toggleDisplay('proofcontrol21')"><span class="show"></span></div>
<div class="proofscript" id="proof21" onclick="toggleDisplay('proof21');toggleDisplay('proofcontrol21')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Example</span> <a id="fold_example2" class="idref" href="#fold_example2"><span class="id" title="definition">fold_example2</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#fold"><span class="id" title="definition">fold</span></a> <a class="idref" href="Basics.html#andb"><span class="id" title="definition">andb</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<div class="togglescript" id="proofcontrol22" onclick="toggleDisplay('proof22');toggleDisplay('proofcontrol22')"><span class="show"></span></div>
<div class="proofscript" id="proof22" onclick="toggleDisplay('proof22');toggleDisplay('proofcontrol22')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Example</span> <a id="fold_example3" class="idref" href="#fold_example3"><span class="id" title="definition">fold_example3</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#fold"><span class="id" title="definition">fold</span></a> <a class="idref" href="Poly.html#app"><span class="id" title="definition">app</span></a>  <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];</span></a><a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;[</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">];[</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]]</span></a> <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<div class="togglescript" id="proofcontrol23" onclick="toggleDisplay('proof23');toggleDisplay('proofcontrol23')"><span class="show"></span></div>
<div class="proofscript" id="proof23" onclick="toggleDisplay('proof23');toggleDisplay('proofcontrol23')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab129"></a><h4 class="section">Exercise: 1 star, advanced (fold_types_different)</h4>
 Observe that the type of <span class="inlinecode"><span class="id" title="tactic">fold</span></span> is parameterized by <i>two</i> type
    variables, <span class="inlinecode"><span class="id" title="var">X</span></span> and <span class="inlinecode"><span class="id" title="var">Y</span></span>, and the parameter <span class="inlinecode"><span class="id" title="var">f</span></span> is a binary operator
    that takes an <span class="inlinecode"><span class="id" title="var">X</span></span> and a <span class="inlinecode"><span class="id" title="var">Y</span></span> and returns a <span class="inlinecode"><span class="id" title="var">Y</span></span>.  Can you think of a
    situation where it would be useful for <span class="inlinecode"><span class="id" title="var">X</span></span> and <span class="inlinecode"><span class="id" title="var">Y</span></span> to be
    different? 
</div>
<div class="code">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_fold_types_different" class="idref" href="#manual_grade_for_fold_types_different"><span class="id" title="definition">manual_grade_for_fold_types_different</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab130"></a><h2 class="section">Functions That Construct Functions</h2>

<div class="paragraph"> </div>

 Most of the higher-order functions we have talked about so
    far take functions as arguments.  Let's look at some examples that
    involve <i>returning</i> functions as the results of other functions.
    To begin, here is a function that takes a value <span class="inlinecode"><span class="id" title="var">x</span></span> (drawn from
    some type <span class="inlinecode"><span class="id" title="var">X</span></span>) and returns a function from <span class="inlinecode"><span class="id" title="var">nat</span></span> to <span class="inlinecode"><span class="id" title="var">X</span></span> that
    yields <span class="inlinecode"><span class="id" title="var">x</span></span> whenever it is called, ignoring its <span class="inlinecode"><span class="id" title="var">nat</span></span> argument. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="constfun" class="idref" href="#constfun"><span class="id" title="definition">constfun</span></a> {<a id="X:163" class="idref" href="#X:163"><span class="id" title="binder">X</span></a>: <span class="id" title="keyword">Type</span>} (<a id="x:164" class="idref" href="#x:164"><span class="id" title="binder">x</span></a>: <a class="idref" href="Poly.html#X:163"><span class="id" title="variable">X</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#X:163"><span class="id" title="variable">X</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<a id="k:165" class="idref" href="#k:165"><span class="id" title="binder">k</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) ⇒ <a class="idref" href="Poly.html#x:164"><span class="id" title="variable">x</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="ftrue" class="idref" href="#ftrue"><span class="id" title="definition">ftrue</span></a> := <a class="idref" href="Poly.html#constfun"><span class="id" title="definition">constfun</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="constfun_example1" class="idref" href="#constfun_example1"><span class="id" title="definition">constfun_example1</span></a> : <a class="idref" href="Poly.html#ftrue"><span class="id" title="definition">ftrue</span></a> 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<div class="togglescript" id="proofcontrol24" onclick="toggleDisplay('proof24');toggleDisplay('proofcontrol24')"><span class="show"></span></div>
<div class="proofscript" id="proof24" onclick="toggleDisplay('proof24');toggleDisplay('proofcontrol24')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Example</span> <a id="constfun_example2" class="idref" href="#constfun_example2"><span class="id" title="definition">constfun_example2</span></a> : (<a class="idref" href="Poly.html#constfun"><span class="id" title="definition">constfun</span></a> 5) 99 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 5.<br/>
<div class="togglescript" id="proofcontrol25" onclick="toggleDisplay('proof25');toggleDisplay('proofcontrol25')"><span class="show"></span></div>
<div class="proofscript" id="proof25" onclick="toggleDisplay('proof25');toggleDisplay('proofcontrol25')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
In fact, the multiple-argument functions we have already
    seen are also examples of passing functions as data.  To see why,
    recall the type of <span class="inlinecode"><span class="id" title="var">plus</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
</div>

<div class="doc">
Each <span class="inlinecode">→</span> in this expression is actually a <i>binary</i> operator
    on types.  This operator is <i>right-associative</i>, so the type of
    <span class="inlinecode"><span class="id" title="var">plus</span></span> is really a shorthand for <span class="inlinecode"><span class="id" title="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode">(<span class="id" title="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">nat</span>)</span> -- i.e., it
    can be read as saying that "<span class="inlinecode"><span class="id" title="var">plus</span></span> is a one-argument function that
    takes a <span class="inlinecode"><span class="id" title="var">nat</span></span> and returns a one-argument function that takes
    another <span class="inlinecode"><span class="id" title="var">nat</span></span> and returns a <span class="inlinecode"><span class="id" title="var">nat</span></span>."  In the examples above, we
    have always applied <span class="inlinecode"><span class="id" title="var">plus</span></span> to both of its arguments at once, but
    if we like we can supply just the first.  This is called <i>partial
    application</i>. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="plus3" class="idref" href="#plus3"><span class="id" title="definition">plus3</span></a> := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> 3.<br/>
<span class="id" title="keyword">Check</span> <a class="idref" href="Poly.html#plus3"><span class="id" title="definition">plus3</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_plus3" class="idref" href="#test_plus3"><span class="id" title="definition">test_plus3</span></a> :    <a class="idref" href="Poly.html#plus3"><span class="id" title="definition">plus3</span></a> 4 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 7.<br/>
<div class="togglescript" id="proofcontrol26" onclick="toggleDisplay('proof26');toggleDisplay('proofcontrol26')"><span class="show"></span></div>
<div class="proofscript" id="proof26" onclick="toggleDisplay('proof26');toggleDisplay('proofcontrol26')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
<span class="id" title="keyword">Example</span> <a id="test_plus3'" class="idref" href="#test_plus3'"><span class="id" title="definition">test_plus3'</span></a> :   <a class="idref" href="Poly.html#doit3times"><span class="id" title="definition">doit3times</span></a> <a class="idref" href="Poly.html#plus3"><span class="id" title="definition">plus3</span></a> 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 9.<br/>
<div class="togglescript" id="proofcontrol27" onclick="toggleDisplay('proof27');toggleDisplay('proofcontrol27')"><span class="show"></span></div>
<div class="proofscript" id="proof27" onclick="toggleDisplay('proof27');toggleDisplay('proofcontrol27')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
<span class="id" title="keyword">Example</span> <a id="test_plus3''" class="idref" href="#test_plus3''"><span class="id" title="definition">test_plus3''</span></a> :  <a class="idref" href="Poly.html#doit3times"><span class="id" title="definition">doit3times</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> 3) 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 9.<br/>
<div class="togglescript" id="proofcontrol28" onclick="toggleDisplay('proof28');toggleDisplay('proofcontrol28')"><span class="show"></span></div>
<div class="proofscript" id="proof28" onclick="toggleDisplay('proof28');toggleDisplay('proofcontrol28')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab131"></a><h1 class="section">Additional Exercises</h1>

</div>
<div class="code">

<span class="id" title="keyword">Module</span> <a id="Exercises" class="idref" href="#Exercises"><span class="id" title="module">Exercises</span></a>.<br/>
</div>

<div class="doc">
<a id="lab132"></a><h4 class="section">Exercise: 2 stars, standard (fold_length)</h4>
 Many common functions on lists can be implemented in terms of
    <span class="inlinecode"><span class="id" title="tactic">fold</span></span>.  For example, here is an alternative definition of <span class="inlinecode"><span class="id" title="var">length</span></span>: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="Exercises.fold_length" class="idref" href="#Exercises.fold_length"><span class="id" title="definition">fold_length</span></a> {<a id="X:166" class="idref" href="#X:166"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>} (<a id="l:167" class="idref" href="#l:167"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:166"><span class="id" title="variable">X</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#fold"><span class="id" title="definition">fold</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> <a id="n:168" class="idref" href="#n:168"><span class="id" title="binder">n</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Poly.html#n:168"><span class="id" title="variable">n</span></a>) <a class="idref" href="Poly.html#l:167"><span class="id" title="variable">l</span></a> 0.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.test_fold_length1" class="idref" href="#Exercises.test_fold_length1"><span class="id" title="definition">test_fold_length1</span></a> : <a class="idref" href="Poly.html#Exercises.fold_length"><span class="id" title="definition">fold_length</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>7<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 3.<br/>
<div class="togglescript" id="proofcontrol29" onclick="toggleDisplay('proof29');toggleDisplay('proofcontrol29')"><span class="show"></span></div>
<div class="proofscript" id="proof29" onclick="toggleDisplay('proof29');toggleDisplay('proofcontrol29')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
Prove the correctness of <span class="inlinecode"><span class="id" title="var">fold_length</span></span>.  (Hint: It may help to
    know that <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span> simplifies expressions a bit more
    aggressively than <span class="inlinecode"><span class="id" title="tactic">simpl</span></span> does -- i.e., you may find yourself in a
    situation where <span class="inlinecode"><span class="id" title="tactic">simpl</span></span> does nothing but <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span> solves the
    goal.) 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="Exercises.fold_length_correct" class="idref" href="#Exercises.fold_length_correct"><span class="id" title="lemma">fold_length_correct</span></a> : <span class="id" title="keyword">∀</span> <a id="X:169" class="idref" href="#X:169"><span class="id" title="binder">X</span></a> (<a id="l:170" class="idref" href="#l:170"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:169"><span class="id" title="variable">X</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#Exercises.fold_length"><span class="id" title="definition">fold_length</span></a> <a class="idref" href="Poly.html#l:170"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#length"><span class="id" title="definition">length</span></a> <a class="idref" href="Poly.html#l:170"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab133"></a><h4 class="section">Exercise: 3 stars, standard (fold_map)</h4>
 We can also define <span class="inlinecode"><span class="id" title="var">map</span></span> in terms of <span class="inlinecode"><span class="id" title="tactic">fold</span></span>.  Finish <span class="inlinecode"><span class="id" title="var">fold_map</span></span>
    below. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="Exercises.fold_map" class="idref" href="#Exercises.fold_map"><span class="id" title="definition">fold_map</span></a> {<a id="X:171" class="idref" href="#X:171"><span class="id" title="binder">X</span></a> <a id="Y:172" class="idref" href="#Y:172"><span class="id" title="binder">Y</span></a>: <span class="id" title="keyword">Type</span>} (<a id="f:173" class="idref" href="#f:173"><span class="id" title="binder">f</span></a>: <a class="idref" href="Poly.html#X:171"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#Y:172"><span class="id" title="variable">Y</span></a>) (<a id="l:174" class="idref" href="#l:174"><span class="id" title="binder">l</span></a>: <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#X:171"><span class="id" title="variable">X</span></a>) : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Poly.html#Y:172"><span class="id" title="variable">Y</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/>
</div>

<div class="doc">
Write down a theorem <span class="inlinecode"><span class="id" title="var">fold_map_correct</span></span> in Coq stating that
   <span class="inlinecode"><span class="id" title="var">fold_map</span></span> is correct, and prove it.  (Hint: again, remember that
   <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span> simplifies expressions a bit more aggressively than
   <span class="inlinecode"><span class="id" title="tactic">simpl</span></span>.) 
</div>
<div class="code">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="Exercises.manual_grade_for_fold_map" class="idref" href="#Exercises.manual_grade_for_fold_map"><span class="id" title="definition">manual_grade_for_fold_map</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab134"></a><h4 class="section">Exercise: 2 stars, advanced (currying)</h4>
 In Coq, a function <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">A</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">B</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">C</span></span> really has the type <span class="inlinecode"><span class="id" title="var">A</span></span>
    <span class="inlinecode">→</span> <span class="inlinecode">(<span class="id" title="var">B</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">C</span>)</span>.  That is, if you give <span class="inlinecode"><span class="id" title="var">f</span></span> a value of type <span class="inlinecode"><span class="id" title="var">A</span></span>, it
    will give you function <span class="inlinecode"><span class="id" title="var">f'</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">B</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">C</span></span>.  If you then give <span class="inlinecode"><span class="id" title="var">f'</span></span> a
    value of type <span class="inlinecode"><span class="id" title="var">B</span></span>, it will return a value of type <span class="inlinecode"><span class="id" title="var">C</span></span>.  This
    allows for partial application, as in <span class="inlinecode"><span class="id" title="var">plus3</span></span>.  Processing a list
    of arguments with functions that return functions is called
    <i>currying</i>, in honor of the logician Haskell Curry.

<div class="paragraph"> </div>

    Conversely, we can reinterpret the type <span class="inlinecode"><span class="id" title="var">A</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">B</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">C</span></span> as <span class="inlinecode">(<span class="id" title="var">A</span></span> <span class="inlinecode">×</span>
    <span class="inlinecode"><span class="id" title="var">B</span>)</span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">C</span></span>.  This is called <i>uncurrying</i>.  With an uncurried binary
    function, both arguments must be given at once as a pair; there is
    no partial application. 
<div class="paragraph"> </div>

 We can define currying as follows: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="Exercises.prod_curry" class="idref" href="#Exercises.prod_curry"><span class="id" title="definition">prod_curry</span></a> {<a id="X:175" class="idref" href="#X:175"><span class="id" title="binder">X</span></a> <a id="Y:176" class="idref" href="#Y:176"><span class="id" title="binder">Y</span></a> <a id="Z:177" class="idref" href="#Z:177"><span class="id" title="binder">Z</span></a> : <span class="id" title="keyword">Type</span>}<br/>
&nbsp;&nbsp;(<a id="f:178" class="idref" href="#f:178"><span class="id" title="binder">f</span></a> : <a class="idref" href="Poly.html#X:175"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Poly.html#Y:176"><span class="id" title="variable">Y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#Z:177"><span class="id" title="variable">Z</span></a>) (<a id="x:179" class="idref" href="#x:179"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#X:175"><span class="id" title="variable">X</span></a>) (<a id="y:180" class="idref" href="#y:180"><span class="id" title="binder">y</span></a> : <a class="idref" href="Poly.html#Y:176"><span class="id" title="variable">Y</span></a>) : <a class="idref" href="Poly.html#Z:177"><span class="id" title="variable">Z</span></a> := <a class="idref" href="Poly.html#f:178"><span class="id" title="variable">f</span></a> <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#x:179"><span class="id" title="variable">x</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Poly.html#y:180"><span class="id" title="variable">y</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a>.<br/>
</div>

<div class="doc">
As an exercise, define its inverse, <span class="inlinecode"><span class="id" title="var">prod_uncurry</span></span>.  Then prove
    the theorems below to show that the two are inverses. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="Exercises.prod_uncurry" class="idref" href="#Exercises.prod_uncurry"><span class="id" title="definition">prod_uncurry</span></a> {<a id="X:181" class="idref" href="#X:181"><span class="id" title="binder">X</span></a> <a id="Y:182" class="idref" href="#Y:182"><span class="id" title="binder">Y</span></a> <a id="Z:183" class="idref" href="#Z:183"><span class="id" title="binder">Z</span></a> : <span class="id" title="keyword">Type</span>}<br/>
&nbsp;&nbsp;(<a id="f:184" class="idref" href="#f:184"><span class="id" title="binder">f</span></a> : <a class="idref" href="Poly.html#X:181"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#Y:182"><span class="id" title="variable">Y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#Z:183"><span class="id" title="variable">Z</span></a>) (<a id="p:185" class="idref" href="#p:185"><span class="id" title="binder">p</span></a> : <a class="idref" href="Poly.html#X:181"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Poly.html#Y:182"><span class="id" title="variable">Y</span></a>) : <a class="idref" href="Poly.html#Z:183"><span class="id" title="variable">Z</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/>
</div>

<div class="doc">
As a (trivial) example of the usefulness of currying, we can use it
    to shorten one of the examples that we saw above: 
</div>
<div class="code">

<span class="id" title="keyword">Example</span> <a id="Exercises.test_map1'" class="idref" href="#Exercises.test_map1'"><span class="id" title="definition">test_map1'</span></a>: <a class="idref" href="Poly.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> 3) <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<div class="togglescript" id="proofcontrol30" onclick="toggleDisplay('proof30');toggleDisplay('proofcontrol30')"><span class="show"></span></div>
<div class="proofscript" id="proof30" onclick="toggleDisplay('proof30');toggleDisplay('proofcontrol30')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
Thought exercise: before running the following commands, can you
    calculate the types of <span class="inlinecode"><span class="id" title="var">prod_curry</span></span> and <span class="inlinecode"><span class="id" title="var">prod_uncurry</span></span>? 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> @<a class="idref" href="Poly.html#Exercises.prod_curry"><span class="id" title="definition">prod_curry</span></a>.<br/>
<span class="id" title="keyword">Check</span> @<a class="idref" href="Poly.html#Exercises.prod_uncurry"><span class="id" title="axiom">prod_uncurry</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="Exercises.uncurry_curry" class="idref" href="#Exercises.uncurry_curry"><span class="id" title="lemma">uncurry_curry</span></a> : <span class="id" title="keyword">∀</span> (<a id="X:186" class="idref" href="#X:186"><span class="id" title="binder">X</span></a> <a id="Y:187" class="idref" href="#Y:187"><span class="id" title="binder">Y</span></a> <a id="Z:188" class="idref" href="#Z:188"><span class="id" title="binder">Z</span></a> : <span class="id" title="keyword">Type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="f:189" class="idref" href="#f:189"><span class="id" title="binder">f</span></a> : <a class="idref" href="Poly.html#X:186"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#Y:187"><span class="id" title="variable">Y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#Z:188"><span class="id" title="variable">Z</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="x:190" class="idref" href="#x:190"><span class="id" title="binder">x</span></a> <a id="y:191" class="idref" href="#y:191"><span class="id" title="binder">y</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#Exercises.prod_curry"><span class="id" title="definition">prod_curry</span></a> (<a class="idref" href="Poly.html#Exercises.prod_uncurry"><span class="id" title="axiom">prod_uncurry</span></a> <a class="idref" href="Poly.html#f:189"><span class="id" title="variable">f</span></a>) <a class="idref" href="Poly.html#x:190"><span class="id" title="variable">x</span></a> <a class="idref" href="Poly.html#y:191"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#f:189"><span class="id" title="variable">f</span></a> <a class="idref" href="Poly.html#x:190"><span class="id" title="variable">x</span></a> <a class="idref" href="Poly.html#y:191"><span class="id" title="variable">y</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="Exercises.curry_uncurry" class="idref" href="#Exercises.curry_uncurry"><span class="id" title="lemma">curry_uncurry</span></a> : <span class="id" title="keyword">∀</span> (<a id="X:192" class="idref" href="#X:192"><span class="id" title="binder">X</span></a> <a id="Y:193" class="idref" href="#Y:193"><span class="id" title="binder">Y</span></a> <a id="Z:194" class="idref" href="#Z:194"><span class="id" title="binder">Z</span></a> : <span class="id" title="keyword">Type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="f:195" class="idref" href="#f:195"><span class="id" title="binder">f</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#X:192"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Poly.html#Y:193"><span class="id" title="variable">Y</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#Z:194"><span class="id" title="variable">Z</span></a>) (<a id="p:196" class="idref" href="#p:196"><span class="id" title="binder">p</span></a> : <a class="idref" href="Poly.html#X:192"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Poly.html#Y:193"><span class="id" title="variable">Y</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#Exercises.prod_uncurry"><span class="id" title="axiom">prod_uncurry</span></a> (<a class="idref" href="Poly.html#Exercises.prod_curry"><span class="id" title="definition">prod_curry</span></a> <a class="idref" href="Poly.html#f:195"><span class="id" title="variable">f</span></a>) <a class="idref" href="Poly.html#p:196"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#f:195"><span class="id" title="variable">f</span></a> <a class="idref" href="Poly.html#p:196"><span class="id" title="variable">p</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab135"></a><h4 class="section">Exercise: 2 stars, advanced (nth_error_informal)</h4>
 Recall the definition of the <span class="inlinecode"><span class="id" title="var">nth_error</span></span> function:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Fixpoint</span> <span class="id" title="var">nth_error</span> {<span class="id" title="var">X</span> : <span class="id" title="keyword">Type</span>} (<span class="id" title="var">l</span> : <span class="id" title="var">list</span> <span class="id" title="var">X</span>) (<span class="id" title="var">n</span> : <span class="id" title="var">nat</span>) : <span class="id" title="var">option</span> <span class="id" title="var">X</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="var">l</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| [] ⇒ <span class="id" title="var">None</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">a</span> :: <span class="id" title="var">l'</span> ⇒ <span class="id" title="keyword">if</span> <span class="id" title="var">n</span> =? <span class="id" title="var">O</span> <span class="id" title="keyword">then</span> <span class="id" title="var">Some</span> <span class="id" title="var">a</span> <span class="id" title="keyword">else</span> <span class="id" title="var">nth_error</span> <span class="id" title="var">l'</span> (<span class="id" title="var">pred</span> <span class="id" title="var">n</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>.
</span>   Write an informal proof of the following theorem:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">X</span> <span class="id" title="var">l</span> <span class="id" title="var">n</span>, <span class="id" title="var">length</span> <span class="id" title="var">l</span> = <span class="id" title="var">n</span> → @<span class="id" title="var">nth_error</span> <span class="id" title="var">X</span> <span class="id" title="var">l</span> <span class="id" title="var">n</span> = <span class="id" title="var">None</span>
</span>
</div>
<div class="code">
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="Exercises.manual_grade_for_informal_proof" class="idref" href="#Exercises.manual_grade_for_informal_proof"><span class="id" title="definition">manual_grade_for_informal_proof</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 The following exercises explore an alternative way of defining
    natural numbers, using the so-called <i>Church numerals</i>, named
    after mathematician Alonzo Church.  We can represent a natural
    number <span class="inlinecode"><span class="id" title="var">n</span></span> as a function that takes a function <span class="inlinecode"><span class="id" title="var">f</span></span> as a parameter
    and returns <span class="inlinecode"><span class="id" title="var">f</span></span> iterated <span class="inlinecode"><span class="id" title="var">n</span></span> times. 
</div>
<div class="code">

<span class="id" title="keyword">Module</span> <a id="Exercises.Church" class="idref" href="#Exercises.Church"><span class="id" title="module">Church</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a id="Exercises.Church.cnat" class="idref" href="#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a> := <span class="id" title="keyword">∀</span> <a id="X:197" class="idref" href="#X:197"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>, <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#X:197"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#X:197"><span class="id" title="variable">X</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#X:197"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#X:197"><span class="id" title="variable">X</span></a>.<br/>
</div>

<div class="doc">
Let's see how to write some numbers with this notation. Iterating
    a function once should be the same as just applying it.  Thus: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="Exercises.Church.one" class="idref" href="#Exercises.Church.one"><span class="id" title="definition">one</span></a> : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<a id="X:198" class="idref" href="#X:198"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>) (<a id="f:199" class="idref" href="#f:199"><span class="id" title="binder">f</span></a> : <a class="idref" href="Poly.html#X:198"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#X:198"><span class="id" title="variable">X</span></a>) (<a id="x:200" class="idref" href="#x:200"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#X:198"><span class="id" title="variable">X</span></a>) ⇒ <a class="idref" href="Poly.html#f:199"><span class="id" title="variable">f</span></a> <a class="idref" href="Poly.html#x:200"><span class="id" title="variable">x</span></a>.<br/>
</div>

<div class="doc">
Similarly, <span class="inlinecode"><span class="id" title="var">two</span></span> should apply <span class="inlinecode"><span class="id" title="var">f</span></span> twice to its argument: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="Exercises.Church.two" class="idref" href="#Exercises.Church.two"><span class="id" title="definition">two</span></a> : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<a id="X:201" class="idref" href="#X:201"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>) (<a id="f:202" class="idref" href="#f:202"><span class="id" title="binder">f</span></a> : <a class="idref" href="Poly.html#X:201"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#X:201"><span class="id" title="variable">X</span></a>) (<a id="x:203" class="idref" href="#x:203"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#X:201"><span class="id" title="variable">X</span></a>) ⇒ <a class="idref" href="Poly.html#f:202"><span class="id" title="variable">f</span></a> (<a class="idref" href="Poly.html#f:202"><span class="id" title="variable">f</span></a> <a class="idref" href="Poly.html#x:203"><span class="id" title="variable">x</span></a>).<br/>
</div>

<div class="doc">
Defining <span class="inlinecode"><span class="id" title="var">zero</span></span> is somewhat trickier: how can we "apply a function
    zero times"?  The answer is actually simple: just return the
    argument untouched. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="Exercises.Church.zero" class="idref" href="#Exercises.Church.zero"><span class="id" title="definition">zero</span></a> : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<a id="X:204" class="idref" href="#X:204"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>) (<a id="f:205" class="idref" href="#f:205"><span class="id" title="binder">f</span></a> : <a class="idref" href="Poly.html#X:204"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#X:204"><span class="id" title="variable">X</span></a>) (<a id="x:206" class="idref" href="#x:206"><span class="id" title="binder">x</span></a> : <a class="idref" href="Poly.html#X:204"><span class="id" title="variable">X</span></a>) ⇒ <a class="idref" href="Poly.html#x:206"><span class="id" title="variable">x</span></a>.<br/>
</div>

<div class="doc">
More generally, a number <span class="inlinecode"><span class="id" title="var">n</span></span> can be written as <span class="inlinecode"><span class="id" title="keyword">fun</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">⇒</span> <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode">(<span class="id" title="var">f</span></span>
    <span class="inlinecode">...</span> <span class="inlinecode">(<span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> <span class="inlinecode">...)</span>, with <span class="inlinecode"><span class="id" title="var">n</span></span> occurrences of <span class="inlinecode"><span class="id" title="var">f</span></span>.  Notice in
    particular how the <span class="inlinecode"><span class="id" title="var">doit3times</span></span> function we've defined previously
    is actually just the Church representation of <span class="inlinecode">3</span>. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="Exercises.Church.three" class="idref" href="#Exercises.Church.three"><span class="id" title="definition">three</span></a> : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a> := @<a class="idref" href="Poly.html#doit3times"><span class="id" title="definition">doit3times</span></a>.<br/>
</div>

<div class="doc">
Complete the definitions of the following functions. Make sure
    that the corresponding unit tests pass by proving them with
    <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span>. 
<div class="paragraph"> </div>

<a id="lab136"></a><h4 class="section">Exercise: 1 star, advanced (church_succ)</h4>

<div class="paragraph"> </div>

 Successor of a natural number: given a Church numeral <span class="inlinecode"><span class="id" title="var">n</span></span>,
    the successor <span class="inlinecode"><span class="id" title="var">succ</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> is a function that iterates its
    argument once more than <span class="inlinecode"><span class="id" title="var">n</span></span>. 
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="Exercises.Church.succ" class="idref" href="#Exercises.Church.succ"><span class="id" title="definition">succ</span></a> (<a id="n:207" class="idref" href="#n:207"><span class="id" title="binder">n</span></a> : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a>) : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.succ_1" class="idref" href="#Exercises.Church.succ_1"><span class="id" title="definition">succ_1</span></a> : <a class="idref" href="Poly.html#Exercises.Church.succ"><span class="id" title="axiom">succ</span></a> <a class="idref" href="Poly.html#Exercises.Church.zero"><span class="id" title="definition">zero</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.one"><span class="id" title="definition">one</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.succ_2" class="idref" href="#Exercises.Church.succ_2"><span class="id" title="definition">succ_2</span></a> : <a class="idref" href="Poly.html#Exercises.Church.succ"><span class="id" title="axiom">succ</span></a> <a class="idref" href="Poly.html#Exercises.Church.one"><span class="id" title="definition">one</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.succ_3" class="idref" href="#Exercises.Church.succ_3"><span class="id" title="definition">succ_3</span></a> : <a class="idref" href="Poly.html#Exercises.Church.succ"><span class="id" title="axiom">succ</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab137"></a><h4 class="section">Exercise: 1 star, advanced (church_plus)</h4>

<div class="paragraph"> </div>

 Addition of two natural numbers: 
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="Exercises.Church.plus" class="idref" href="#Exercises.Church.plus"><span class="id" title="definition">plus</span></a> (<a id="n:208" class="idref" href="#n:208"><span class="id" title="binder">n</span></a> <a id="m:209" class="idref" href="#m:209"><span class="id" title="binder">m</span></a> : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a>) : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.plus_1" class="idref" href="#Exercises.Church.plus_1"><span class="id" title="definition">plus_1</span></a> : <a class="idref" href="Poly.html#Exercises.Church.plus"><span class="id" title="axiom">plus</span></a> <a class="idref" href="Poly.html#Exercises.Church.zero"><span class="id" title="definition">zero</span></a> <a class="idref" href="Poly.html#Exercises.Church.one"><span class="id" title="definition">one</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.one"><span class="id" title="definition">one</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.plus_2" class="idref" href="#Exercises.Church.plus_2"><span class="id" title="definition">plus_2</span></a> : <a class="idref" href="Poly.html#Exercises.Church.plus"><span class="id" title="axiom">plus</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.plus"><span class="id" title="axiom">plus</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.plus_3" class="idref" href="#Exercises.Church.plus_3"><span class="id" title="definition">plus_3</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#Exercises.Church.plus"><span class="id" title="axiom">plus</span></a> (<a class="idref" href="Poly.html#Exercises.Church.plus"><span class="id" title="axiom">plus</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a>) <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.plus"><span class="id" title="axiom">plus</span></a> <a class="idref" href="Poly.html#Exercises.Church.one"><span class="id" title="definition">one</span></a> (<a class="idref" href="Poly.html#Exercises.Church.plus"><span class="id" title="axiom">plus</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a>).<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab138"></a><h4 class="section">Exercise: 2 stars, advanced (church_mult)</h4>

<div class="paragraph"> </div>

 Multiplication: 
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="Exercises.Church.mult" class="idref" href="#Exercises.Church.mult"><span class="id" title="definition">mult</span></a> (<a id="n:210" class="idref" href="#n:210"><span class="id" title="binder">n</span></a> <a id="m:211" class="idref" href="#m:211"><span class="id" title="binder">m</span></a> : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a>) : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.mult_1" class="idref" href="#Exercises.Church.mult_1"><span class="id" title="definition">mult_1</span></a> : <a class="idref" href="Poly.html#Exercises.Church.mult"><span class="id" title="axiom">mult</span></a> <a class="idref" href="Poly.html#Exercises.Church.one"><span class="id" title="definition">one</span></a> <a class="idref" href="Poly.html#Exercises.Church.one"><span class="id" title="definition">one</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.one"><span class="id" title="definition">one</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.mult_2" class="idref" href="#Exercises.Church.mult_2"><span class="id" title="definition">mult_2</span></a> : <a class="idref" href="Poly.html#Exercises.Church.mult"><span class="id" title="axiom">mult</span></a> <a class="idref" href="Poly.html#Exercises.Church.zero"><span class="id" title="definition">zero</span></a> (<a class="idref" href="Poly.html#Exercises.Church.plus"><span class="id" title="axiom">plus</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.zero"><span class="id" title="definition">zero</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.mult_3" class="idref" href="#Exercises.Church.mult_3"><span class="id" title="definition">mult_3</span></a> : <a class="idref" href="Poly.html#Exercises.Church.mult"><span class="id" title="axiom">mult</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.plus"><span class="id" title="axiom">plus</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab139"></a><h4 class="section">Exercise: 2 stars, advanced (church_exp)</h4>

<div class="paragraph"> </div>

 Exponentiation: 
<div class="paragraph"> </div>

 (<i>Hint</i>: Polymorphism plays a crucial role here.  However,
    choosing the right type to iterate over can be tricky.  If you hit
    a "Universe inconsistency" error, try iterating over a different
    type.  Iterating over <span class="inlinecode"><span class="id" title="var">cnat</span></span> itself is usually problematic.) 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="Exercises.Church.exp" class="idref" href="#Exercises.Church.exp"><span class="id" title="definition">exp</span></a> (<a id="n:212" class="idref" href="#n:212"><span class="id" title="binder">n</span></a> <a id="m:213" class="idref" href="#m:213"><span class="id" title="binder">m</span></a> : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a>) : <a class="idref" href="Poly.html#Exercises.Church.cnat"><span class="id" title="definition">cnat</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.exp_1" class="idref" href="#Exercises.Church.exp_1"><span class="id" title="definition">exp_1</span></a> : <a class="idref" href="Poly.html#Exercises.Church.exp"><span class="id" title="axiom">exp</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.plus"><span class="id" title="axiom">plus</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.exp_2" class="idref" href="#Exercises.Church.exp_2"><span class="id" title="definition">exp_2</span></a> : <a class="idref" href="Poly.html#Exercises.Church.exp"><span class="id" title="axiom">exp</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a> <a class="idref" href="Poly.html#Exercises.Church.zero"><span class="id" title="definition">zero</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.one"><span class="id" title="definition">one</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="Exercises.Church.exp_3" class="idref" href="#Exercises.Church.exp_3"><span class="id" title="definition">exp_3</span></a> : <a class="idref" href="Poly.html#Exercises.Church.exp"><span class="id" title="axiom">exp</span></a> <a class="idref" href="Poly.html#Exercises.Church.three"><span class="id" title="definition">three</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#Exercises.Church.plus"><span class="id" title="axiom">plus</span></a> (<a class="idref" href="Poly.html#Exercises.Church.mult"><span class="id" title="axiom">mult</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a> (<a class="idref" href="Poly.html#Exercises.Church.mult"><span class="id" title="axiom">mult</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a> <a class="idref" href="Poly.html#Exercises.Church.two"><span class="id" title="definition">two</span></a>)) <a class="idref" href="Poly.html#Exercises.Church.one"><span class="id" title="definition">one</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="code">

<span class="id" title="keyword">End</span> <a class="idref" href="Poly.html#Exercises.Church"><span class="id" title="module">Church</span></a>.<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Poly.html#Exercises"><span class="id" title="module">Exercises</span></a>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;2021-08-11&nbsp;15:08&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>